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-7pb.opb
MD5SUM	24909033929a72aa74b2fd8b12f27bce
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	64
Optimality of the best value was proved	NO
Number of terms in the objective function	672
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	672
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	672
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.02884
Number of variables	672
Total number of constraints	2030
Number of constraints which are clauses	2006
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	28
Trace number 5139

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 22:23:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3627 boxname=wulflinc12 idbench=243 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24909033929a72aa74b2fd8b12f27bce  /oldhome/oroussel/tmp/wulflinc12/normalized-s4-4-3-7pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-s4-4-3-7pb.opb /oldhome/oroussel/tmp/wulflinc12/normalized-s4-4-3-7pb.opb
IDLAUNCH: 3627
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        919400 kB
Buffers:         34764 kB
Cached:          61304 kB
SwapCached:         16 kB
Active:          59540 kB
Inactive:        39440 kB
HighTotal:      131008 kB
HighFree:        65800 kB
LowTotal:       903652 kB
LowFree:        853600 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10680 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:30:23 (client local time) WITH STATUS 30 IN 416.997 SECONDS
stats: 3627 0 416.997 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2030 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2016]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1991]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1969]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1959]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1941]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1919]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1893]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1887]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1877]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1867]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1817]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1815]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1813]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1769]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1743]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1729]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1703]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1681]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1671]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1665]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1647]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1609]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1582]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1560]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1534]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1528]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1500]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1482]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1456]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1436]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1386]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1384]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1366]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1344]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1318]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1284]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1266]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1216]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1122]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1094]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1068]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1050]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1024]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1014]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1004]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 954]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 952]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 934]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 912]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 886]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 880]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 870]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 860]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 809]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 799]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 789]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 739]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 737]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 684]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 617]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 607]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 595]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 542]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 487]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 465]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 459]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 435]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 387]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 304]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 286]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 248]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 224]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 198]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 176]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 104]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  98]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  94]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  68]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  50]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  22]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  21]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  20]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  19]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  18]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  17]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  16]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  15]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  14]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  13]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  12]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  11]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[  10]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   9]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   8]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   7]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   6]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   5]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   4]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   3]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   2]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   1]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ---[   0]---> Adder-cost: 50   maxlim: 24   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9846    34000 |    3282       0        0     nan |  0.000 % |
c |       100 |    9839    33977 |    3610      99      484     4.9 | 19.193 % |
c |       250 |    9784    33798 |    3971     239     1204     5.0 | 19.637 % |
c |       475 |    9750    33688 |    4368     458     2285     5.0 | 19.947 % |
c |       814 |    9662    33394 |    4805     775     4278     5.5 | 20.567 % |
c |      1320 |    9535    32969 |    5285    1246     7556     6.1 | 21.454 % |
c |      2079 |    9369    32407 |    5814    1953    14255     7.3 | 22.606 % |
c |      3218 |    9183    31779 |    6395    3023    24063     8.0 | 23.892 % |
c |      4926 |    8928    30918 |    7035    4674    45793     9.8 | 25.709 % |
c |      7488 |    8826    30570 |    7738    7156    92470    12.9 | 26.418 % |
c |     11334 |    8689    30105 |    8512    6303   131002    20.8 | 27.305 % |
c |     17101 |    8670    30042 |    9363    7411   171997    23.2 | 27.394 % |
c |     25752 |    8610    29839 |   10300    5973    84771    14.2 | 27.793 % |
c |     38728 |    8246    28602 |   11330    7825   137560    17.6 | 30.053 % |
c |     58189 |    8222    28520 |   12463    9119   122987    13.5 | 30.186 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1246   maxlim: 557   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73875 |   16744    58992 |    5581   11524   180563    15.7 | 30.186 % |
c |     73976 |   16744    58992 |    6139    5863   102625    17.5 | 20.228 % |
c |     74127 |   16744    58992 |    6753    6014   104863    17.4 | 20.228 % |
c |     74352 |   16744    58992 |    7428    6239   108205    17.3 | 20.228 % |
c |     74690 |   16744    58992 |    8171    6577   114367    17.4 | 20.228 % |
c |     75196 |   16744    58992 |    8988    7083   124441    17.6 | 20.228 % |
c |     75955 |   16744    58992 |    9887    7842   140457    17.9 | 20.228 % |
c |     77096 |   16738    58972 |   10875    8981   161361    18.0 | 20.257 % |
c |     78804 |   16738    58972 |   11963   10689   190937    17.9 | 20.257 % |
c |     81367 |   16731    58949 |   13159    6837   103493    15.1 | 20.285 % |
c |     85211 |   16731    58949 |   14475   10681   175215    16.4 | 20.285 % |
c |     90977 |   16731    58949 |   15923    8763   123709    14.1 | 20.285 % |
c |     99629 |   16722    58920 |   17515    9007   135877    15.1 | 20.342 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 559   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110245 |   16723    58924 |    5574   19623  1236153    63.0 | 20.342 % |
c |    110346 |   16723    58924 |    6131    5007   621497   124.1 | 20.365 % |
c |    110497 |   16723    58924 |    6744    5158   622714   120.7 | 20.365 % |
c |    110723 |   16723    58924 |    7418    5384   624951   116.1 | 20.365 % |
c |    111060 |   16723    58924 |    8160    5721   630938   110.3 | 20.365 % |
c |    111566 |   16713    58886 |    8976    6224   637910   102.5 | 20.394 % |
c |    112326 |   16704    58855 |    9874    6981   647284    92.7 | 20.422 % |
c |    113465 |   16704    58855 |   10862    8120   671199    82.7 | 20.422 % |
c |    115175 |   16695    58824 |   11948    9827   699959    71.2 | 20.451 % |
c |    117738 |   16686    58793 |   13143   12388   745306    60.2 | 20.479 % |
c |    121585 |   16665    58720 |   14457    9180   152202    16.6 | 20.565 % |
c |    127352 |   16647    58658 |   15903   14931   286685    19.2 | 20.622 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 561   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135194 |   16652    58681 |    5550   14438   262508    18.2 | 20.622 % |
c |    135295 |   16652    58681 |    6105    3711    44979    12.1 | 20.644 % |
c |    135446 |   16652    58681 |    6715    3862    48416    12.5 | 20.644 % |
c |    135673 |   16652    58681 |    7387    4089    52104    12.7 | 20.644 % |
c |    136011 |   16643    58650 |    8125    4425    58207    13.2 | 20.673 % |
c |    136517 |   16643    58650 |    8938    4931    67482    13.7 | 20.673 % |
c |    137276 |   16643    58650 |    9832    5690    82493    14.5 | 20.673 % |
c |    138416 |   16643    58650 |   10815    6830   116747    17.1 | 20.673 % |
c |    140124 |   16624    58583 |   11896    8527   146081    17.1 | 20.759 % |
c |    142686 |   16624    58583 |   13086   11089   210917    19.0 | 20.758 % |
c |    146531 |   16624    58583 |   14395    7992   148526    18.6 | 20.758 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 563   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149618 |   16625    58589 |    5541   11079   210856    19.0 | 20.758 % |
c |    149718 |   16625    58589 |    6095    5640    79131    14.0 | 20.781 % |
c |    149868 |   16625    58589 |    6704    5790    82406    14.2 | 20.781 % |
c |    150093 |   16625    58589 |    7375    6015    87412    14.5 | 20.781 % |
c |    150430 |   16625    58589 |    8112    6352    95581    15.0 | 20.781 % |
c |    150936 |   16625    58589 |    8923    6858   111140    16.2 | 20.781 % |
c |    151697 |   16625    58589 |    9816    7619   127758    16.8 | 20.781 % |
c |    152836 |   16625    58589 |   10797    8758   149760    17.1 | 20.781 % |
c |    154544 |   16625    58589 |   11877   10466   219657    21.0 | 20.781 % |
c |    157106 |   16625    58589 |   13065   13028   355170    27.3 | 20.781 % |
c |    160950 |   16625    58589 |   14371    9625   423935    44.0 | 20.781 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 565   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    164761 |   16626    58596 |    5542   13436   798646    59.4 | 20.781 % |
c |    164861 |   16626    58596 |    6096    3459   182615    52.8 | 20.804 % |
c |    165011 |   16626    58596 |    6705    3609   184457    51.1 | 20.804 % |
c |    165238 |   16626    58596 |    7376    3836   187144    48.8 | 20.804 % |
c |    165575 |   16626    58596 |    8114    4173   191613    45.9 | 20.804 % |
c |    166082 |   16626    58596 |    8925    4680   199214    42.6 | 20.804 % |
c |    166841 |   16626    58596 |    9817    5439   214101    39.4 | 20.804 % |
c |    167981 |   16626    58596 |   10799    6579   236276    35.9 | 20.804 % |
c |    169689 |   16626    58596 |   11879    8287   270441    32.6 | 20.804 % |
c |    172251 |   16620    58576 |   13067   10848   315581    29.1 | 20.832 % |
c |    176096 |   16620    58576 |   14374    7580   107354    14.2 | 20.832 % |
c |    181862 |   16590    58469 |   15811   13247   251699    19.0 | 20.889 % |
c |    190511 |   16590    58469 |   17393   13011   763736    58.7 | 20.889 % |
c |    203485 |   16590    58469 |   19132   16878   800285    47.4 | 20.889 % |
c |    222948 |   16579    58430 |   21045   16346  1357988    83.1 | 20.946 % |
c |    252142 |   16573    58410 |   23150   12150  1114503    91.7 | 20.975 % |
c |    295931 |   16557    58352 |   25465   19053  1009300    53.0 | 21.032 % |
c |    361617 |   16463    58020 |   28011   16938  1028651    60.7 | 21.260 % |
c ==============================================================================
c [1mOptimal solution: 64[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
c _______________________________________________________________________________
c 
c restarts              : 80
c conflicts             : 408406         (980 /sec)
c decisions             : 832330         (1997 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 416.821 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.91 0.95 0.90 2/54 28855
Raw data (stat): 28855 (runsolver) R 28854 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421297793 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.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 944 0 0 0 996 1 0 0 25 0 1 0 421297793 5492736 922 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1341 922 603 41 0 1300 0
vsize: 5364
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 1053 0 0 0 1994 2 0 0 25 0 1 0 421297793 6037504 1031 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1474 1031 603 41 0 1433 0
vsize: 5896
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 1253 0 0 0 2993 3 0 0 25 0 1 0 421297793 6742016 1231 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1646 1231 603 41 0 1605 0
vsize: 6584
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 1637 0 0 0 3991 4 0 0 25 0 1 0 421297793 8433664 1615 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2059 1615 603 41 0 2018 0
vsize: 8236
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 4990 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 5990 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 6989 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+80.0051 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 7990 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223760 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+90.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 8990 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 9990 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223664 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2386 0 0 0 10990 6 0 0 25 0 1 0 421297793 11530240 2364 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2815 2364 603 41 0 2774 0
vsize: 11260
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2665 0 0 0 11989 8 0 0 25 0 1 0 421297793 12595200 2643 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3075 2643 603 41 0 3034 0
vsize: 12300
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 2856 0 0 0 12989 8 0 0 25 0 1 0 421297793 13402112 2834 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3272 2834 603 41 0 3231 0
vsize: 13088
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 3354 0 0 0 13987 10 0 0 25 0 1 0 421297793 15409152 3332 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3332 603 41 0 3721 0
vsize: 15048
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 3354 0 0 0 14987 10 0 0 25 0 1 0 421297793 15409152 3332 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3332 603 41 0 3721 0
vsize: 15048
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 3354 0 0 0 15987 10 0 0 25 0 1 0 421297793 15409152 3332 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3332 603 41 0 3721 0
vsize: 15048
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 3354 0 0 0 16988 10 0 0 25 0 1 0 421297793 15409152 3332 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3332 603 41 0 3721 0
vsize: 15048
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 3425 0 0 0 17987 11 0 0 25 0 1 0 421297793 15679488 3403 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3828 3403 603 41 0 3787 0
vsize: 15312
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 3562 0 0 0 18987 11 0 0 25 0 1 0 421297793 16347136 3540 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3540 603 41 0 3950 0
vsize: 15964
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4301 0 0 0 19985 13 0 0 25 0 1 0 421297793 19283968 4279 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4708 4279 603 41 0 4667 0
vsize: 18832
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4360 0 0 0 20985 13 0 0 25 0 1 0 421297793 19550208 4338 4294967295 134512640 134672761 3221224560 3221223700 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4338 603 41 0 4732 0
vsize: 19092
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4364 0 0 0 21985 13 0 0 25 0 1 0 421297793 19550208 4342 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4342 603 41 0 4732 0
vsize: 19092
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4365 0 0 0 22985 13 0 0 25 0 1 0 421297793 19550208 4343 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4343 603 41 0 4732 0
vsize: 19092
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4366 0 0 0 23985 13 0 0 25 0 1 0 421297793 19550208 4344 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4344 603 41 0 4732 0
vsize: 19092
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4366 0 0 0 24986 13 0 0 25 0 1 0 421297793 19550208 4344 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4344 603 41 0 4732 0
vsize: 19092
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4366 0 0 0 25986 13 0 0 25 0 1 0 421297793 19550208 4344 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4344 603 41 0 4732 0
vsize: 19092
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4366 0 0 0 26986 13 0 0 25 0 1 0 421297793 19550208 4344 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4344 603 41 0 4732 0
vsize: 19092
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4366 0 0 0 27986 13 0 0 25 0 1 0 421297793 19550208 4344 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4344 603 41 0 4732 0
vsize: 19092
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4366 0 0 0 28986 13 0 0 25 0 1 0 421297793 19550208 4344 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4344 603 41 0 4732 0
vsize: 19092
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 4648 0 0 0 29986 14 0 0 25 0 1 0 421297793 20754432 4626 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5067 4626 603 41 0 5026 0
vsize: 20268
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5134 0 0 0 30985 15 0 0 25 0 1 0 421297793 22761472 5112 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5112 603 41 0 5516 0
vsize: 22228
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5134 0 0 0 31985 15 0 0 25 0 1 0 421297793 22761472 5112 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5112 603 41 0 5516 0
vsize: 22228
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5134 0 0 0 32985 15 0 0 25 0 1 0 421297793 22761472 5112 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5112 603 41 0 5516 0
vsize: 22228
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5134 0 0 0 33985 15 0 0 25 0 1 0 421297793 22761472 5112 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5112 603 41 0 5516 0
vsize: 22228
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5137 0 0 0 34986 15 0 0 25 0 1 0 421297793 22761472 5115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5115 603 41 0 5516 0
vsize: 22228
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5137 0 0 0 35986 15 0 0 25 0 1 0 421297793 22761472 5115 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5115 603 41 0 5516 0
vsize: 22228
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5137 0 0 0 36986 15 0 0 25 0 1 0 421297793 22761472 5115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5115 603 41 0 5516 0
vsize: 22228
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5137 0 0 0 37986 15 0 0 25 0 1 0 421297793 22761472 5115 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5557 5115 603 41 0 5516 0
vsize: 22228
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5206 0 0 0 38986 16 0 0 25 0 1 0 421297793 23031808 5184 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5623 5184 603 41 0 5582 0
vsize: 22492
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5206 0 0 0 39986 16 0 0 25 0 1 0 421297793 23031808 5184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5623 5184 603 41 0 5582 0
vsize: 22492
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5210 0 0 0 40986 16 0 0 25 0 1 0 421297793 23031808 5188 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5623 5188 603 41 0 5582 0
vsize: 22492
[startup+416.979 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 28855
Raw data (stat): 28855 (minisat+) R 28854 25285 25284 0 -1 0 5210 0 0 0 40986 16 0 0 25 0 1 0 421297793 23031808 5188 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5623 5188 603 41 0 5582 0
vsize: 0

Child status: 30
Real time (s): 416.978
CPU time (s): 416.997
CPU user time (s): 416.823
CPU system time (s): 0.173973
CPU usage (%): 100.004
Max. virtual memory (Kb): 22492
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	64
#### END VERIFIER DATA ####