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-8pb.opb
MD5SUM	2bf0a3299a380a62e2f4aaf6d6f8fe18
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	36
Optimality of the best value was proved	NO
Number of terms in the objective function	432
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	432
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	432
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.903861
Number of variables	432
Total number of constraints	1304
Number of constraints which are clauses	1280
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	18

Trace number 6266

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 04:21:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4756 boxname=wulflinc31 idbench=244 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2bf0a3299a380a62e2f4aaf6d6f8fe18  /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-8pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-8pb.opb /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-8pb.opb
IDLAUNCH: 4756
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888320 kB
Buffers:         36348 kB
Cached:          71312 kB
SwapCached:        392 kB
Active:          52252 kB
Inactive:        58592 kB
HighTotal:      131008 kB
HighFree:        56028 kB
LowTotal:       903652 kB
LowFree:        832292 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            30008 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:22:37 (client local time) WITH STATUS 30 IN 58.893 SECONDS
stats: 4756 0 58.893 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1304 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1290]---> BDD-cost:    1
c ---[1264]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1232]---> BDD-cost:    1
c ---[1199]---> BDD-cost:    1
c ---[1173]---> BDD-cost:    1
c ---[1171]---> BDD-cost:    1
c ---[1161]---> BDD-cost:    1
c ---[1147]---> BDD-cost:    1
c ---[1121]---> BDD-cost:    1
c ---[1099]---> BDD-cost:    1
c ---[1089]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1030]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1018]---> BDD-cost:    1
c ---[1008]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:    1
c ---[ 948]---> BDD-cost:    1
c ---[ 946]---> BDD-cost:    1
c ---[ 932]---> BDD-cost:    1
c ---[ 906]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 874]---> BDD-cost:    1
c ---[ 826]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 806]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 802]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 758]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 663]---> BDD-cost:    1
c ---[ 661]---> BDD-cost:    1
c ---[ 643]---> BDD-cost:    1
c ---[ 622]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 590]---> BDD-cost:    1
c ---[ 554]---> BDD-cost:    1
c ---[ 532]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 520]---> BDD-cost:    1
c ---[ 518]---> BDD-cost:    1
c ---[ 492]---> BDD-cost:    1
c ---[ 474]---> BDD-cost:    1
c ---[ 448]---> BDD-cost:    1
c ---[ 430]---> BDD-cost:    1
c ---[ 408]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 366]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:    1
c ---[ 305]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   59
c ---[  22]---> BDD-cost:   59
c ---[  21]---> BDD-cost:   59
c ---[  20]---> BDD-cost:   59
c ---[  19]---> BDD-cost:   59
c ---[  18]---> BDD-cost:   59
c ---[  17]---> BDD-cost:   59
c ---[  16]---> BDD-cost:   59
c ---[  15]---> BDD-cost:   59
c ---[  14]---> BDD-cost:   59
c ---[  13]---> BDD-cost:   59
c ---[  12]---> BDD-cost:   59
c ---[  11]---> BDD-cost:   59
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   59
c ---[   8]---> BDD-cost:   59
c ---[   7]---> BDD-cost:   59
c ---[   6]---> BDD-cost:   59
c ---[   5]---> BDD-cost:   59
c ---[   4]---> BDD-cost:   59
c ---[   3]---> BDD-cost:   59
c ---[   2]---> BDD-cost:   59
c ---[   1]---> BDD-cost:   59
c ---[   0]---> BDD-cost:   59
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8480    24720 |    2826       0        0     nan |  0.000 % |
c |       100 |    8480    24720 |    3108     100     2698    27.0 |  5.000 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16194     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       176 |   44715   109574 |   14905     176     4271    24.3 |  5.000 % |
c |       276 |   44715   109574 |   16395     276     6360    23.0 |  1.466 % |
c |       428 |   44639   109404 |   18035     426    10508    24.7 |  1.609 % |
c |       654 |   44639   109404 |   19838     652    15040    23.1 |  1.609 % |
c |       991 |   44639   109404 |   21822     989    24612    24.9 |  1.609 % |
c |      1498 |   44639   109404 |   24004    1496    36525    24.4 |  1.609 % |
c |      2261 |   44639   109404 |   26405    2259    55296    24.5 |  1.609 % |
c |      3401 |   44639   109404 |   29045    3399    85488    25.2 |  1.609 % |
c |      5109 |   43563   106974 |   31950    5068   122817    24.2 |  3.739 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6326 |   42816   105291 |   14272    6275   148335    23.6 |  3.739 % |
c |      6426 |   42816   105291 |   15699    6375   150452    23.6 |  5.446 % |
c |      6577 |   42816   105291 |   17269    6526   154631    23.7 |  5.447 % |
c |      6802 |   42816   105291 |   18996    6751   159072    23.6 |  5.447 % |
c |      7139 |   42816   105291 |   20895    7088   164886    23.3 |  5.447 % |
c |      7645 |   42816   105291 |   22985    7594   173295    22.8 |  5.447 % |
c |      8405 |   42816   105291 |   25283    8354   187074    22.4 |  5.447 % |
c |      9544 |   42816   105291 |   27812    9493   208538    22.0 |  5.447 % |
c |     11254 |   42816   105291 |   30593   11203   234405    20.9 |  5.447 % |
c |     13816 |   41357   101960 |   33652   13738   273094    19.9 |  8.480 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17289 |   39725    98216 |   13241   17091   320779    18.8 |  8.480 % |
c |     17391 |   39725    98216 |   14565    8648   117689    13.6 | 12.024 % |
c |     17541 |   39725    98216 |   16021    8798   121317    13.8 | 12.024 % |
c |     17766 |   39451    97587 |   17623    9013   123156    13.7 | 12.609 % |
c |     18105 |   39395    97459 |   19386    9351   128086    13.7 | 12.730 % |
c |     18611 |   39395    97459 |   21324    9857   140060    14.2 | 12.730 % |
c |     19370 |   39058    96680 |   23457   10594   150065    14.2 | 13.472 % |
c ==============================================================================
c [1mFound solution: 56[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19600 |   36925    91785 |   12308   10813   157786    14.6 | 13.472 % |
c |     19701 |   36909    91748 |   13538   10899   158388    14.5 | 18.331 % |
c |     19851 |   36887    91698 |   14892   11045   159400    14.4 | 18.374 % |
c |     20077 |   36838    91586 |   16381   11265   161236    14.3 | 18.481 % |
c |     20416 |   36592    91019 |   18020   11595   164998    14.2 | 19.015 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20786 |   36549    90914 |   12183   11954   169963    14.2 | 19.015 % |
c |     20887 |   36523    90855 |   13401   12051   170775    14.2 | 19.233 % |
c |     21037 |   36329    90399 |   14741   12183   172312    14.1 | 19.695 % |
c |     21262 |   35998    89628 |   16215   12393   174185    14.1 | 20.450 % |
c |     21600 |   35943    89499 |   17837   12724   180338    14.2 | 20.578 % |
c |     22106 |   34590    86361 |   19620   13168   184416    14.0 | 23.674 % |
c |     22865 |   34590    86361 |   21582   13927   202693    14.6 | 23.674 % |
c |     24004 |   34353    85804 |   23741   14912   227104    15.2 | 24.151 % |
c |     25713 |   34294    85667 |   26115   16619   263989    15.9 | 24.301 % |
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7156     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27691 |   44214   108831 |   14738   18597   306484    16.5 | 24.301 % |
c |     27791 |   44214   108831 |   16211    9399   152937    16.3 | 20.621 % |
c |     27941 |   44214   108831 |   17832    9549   155851    16.3 | 20.621 % |
c |     28166 |   44128   108640 |   19616    9772   159862    16.4 | 20.769 % |
c |     28503 |   44128   108640 |   21577   10109   165944    16.4 | 20.769 % |
c |     29009 |   44128   108640 |   23735   10615   176135    16.6 | 20.769 % |
c |     29768 |   44128   108640 |   26109   11374   192699    16.9 | 20.769 % |
c |     30908 |   44128   108640 |   28720   12514   218282    17.4 | 20.769 % |
c ==============================================================================
c [1mFound solution: 50[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32252 |   43727   107727 |   14575   13856   246232    17.8 | 20.769 % |
c |     32352 |   43673   107603 |   16032   13955   247703    17.8 | 21.653 % |
c |     32502 |   43614   107471 |   17635   14101   251335    17.8 | 21.750 % |
c |     32728 |   43614   107471 |   19399   14327   255526    17.8 | 21.750 % |
c |     33067 |   43614   107471 |   21339   14666   262331    17.9 | 21.750 % |
c |     33574 |   43563   107357 |   23473   15172   272437    18.0 | 21.835 % |
c |     34333 |   43563   107357 |   25820   15931   286472    18.0 | 21.835 % |
c ==============================================================================
c [1mFound solution: 48[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34775 |   43559   107346 |   14519   16373   294513    18.0 | 21.835 % |
c |     34877 |   43559   107346 |   15970   16475   296937    18.0 | 21.900 % |
c |     35027 |   43559   107346 |   17567   16625   300241    18.1 | 21.900 % |
c |     35253 |   43559   107346 |   19324   16851   304829    18.1 | 21.900 % |
c |     35592 |   43541   107305 |   21257   17187   310896    18.1 | 21.928 % |
c |     36099 |   43450   107099 |   23382   17690   319512    18.1 | 22.082 % |
c ==============================================================================
c [1mFound solution: 46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36278 |   37227    92723 |   12409   17481   310191    17.7 | 22.082 % |
c |     36379 |   37227    92723 |   13649   17582   312024    17.7 | 33.743 % |
c |     36530 |   37227    92723 |   15014   17733   314498    17.7 | 33.743 % |
c |     36755 |   37227    92723 |   16516   17958   318991    17.8 | 33.743 % |
c |     37092 |   37227    92723 |   18168   18295   324410    17.7 | 33.743 % |
c ==============================================================================
c [1mFound solution: 44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37395 |   37212    92684 |   12404   18597   329168    17.7 | 33.743 % |
c |     37495 |   37212    92684 |   13644    9399   137044    14.6 | 33.818 % |
c ==============================================================================
c [1mFound solution: 42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37618 |   37026    92239 |   12342    8973   126977    14.2 | 33.818 % |
c |     37718 |   37026    92239 |   13576    9073   128271    14.1 | 34.251 % |
c |     37871 |   37026    92239 |   14933    9226   130403    14.1 | 34.251 % |
c |     38096 |   37026    92239 |   16427    9451   133642    14.1 | 34.251 % |
c ==============================================================================
c [1mFound solution: 40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38292 |   37013    92204 |   12337    9640   135820    14.1 | 34.251 % |
c ==============================================================================
c [1mFound solution: 38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38297 |   27406    69654 |    9135    8508   117844    13.9 | 34.251 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c [1mOptimal solution: 36[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
c _______________________________________________________________________________
c 
c restarts              : 76
c conflicts             : 38297          (651 /sec)
c decisions             : 70521          (1199 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 58.8091 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.84 0.97 0.93 2/54 31146
Raw data (stat): 31146 (runsolver) R 31145 23176 23175 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 481658722 1052672 97 4294967295 134512640 135381576 3221224464 3221219904 134514522 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99987 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 31146
Raw data (stat): 31146 (minisat+) R 31145 23176 23175 0 -1 0 1917 0 0 0 993 5 0 0 25 0 1 0 481658722 9736192 1890 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2377 1890 603 41 0 2336 0
vsize: 9508
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 31146
Raw data (stat): 31146 (minisat+) R 31145 23176 23175 0 -1 0 2023 0 0 0 1992 5 0 0 25 0 1 0 481658722 10256384 1996 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2504 1996 603 41 0 2463 0
vsize: 10016
[startup+30.0009 s]
Raw data (loadavg): 0.90 0.97 0.93 2/54 31146
Raw data (stat): 31146 (minisat+) R 31145 23176 23175 0 -1 0 2023 0 0 0 2992 5 0 0 25 0 1 0 481658722 10256384 1996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2504 1996 603 41 0 2463 0
vsize: 10016
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 31146
Raw data (stat): 31146 (minisat+) R 31145 23176 23175 0 -1 0 2381 0 0 0 3991 6 0 0 25 0 1 0 481658722 12009472 2311 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2932 2311 603 41 0 2891 0
vsize: 11728
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 31146
Raw data (stat): 31146 (minisat+) R 31145 23176 23175 0 -1 0 2428 0 0 0 4991 6 0 0 25 0 1 0 481658722 12263424 2358 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2358 603 41 0 2953 0
vsize: 11976
[startup+58.9116 s]
Raw data (loadavg): 0.94 0.97 0.93 1/53 31146
Raw data (stat): 31146 (minisat+) R 31145 23176 23175 0 -1 0 2428 0 0 0 4991 6 0 0 25 0 1 0 481658722 12263424 2358 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2358 603 41 0 2953 0
vsize: 0

Child status: 30
Real time (s): 58.911
CPU time (s): 58.893
CPU user time (s): 58.8171
CPU system time (s): 0.075988
CPU usage (%): 99.9695
Max. virtual memory (Kb): 11976
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	36
#### END VERIFIER DATA ####