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-4pb.opb
MD5SUM	c1a86b94297136b91215b2ae8a8f5643
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	60
Optimality of the best value was proved	NO
Number of terms in the objective function	696
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	696
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	696
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.03784
Number of variables	696
Total number of constraints	2096
Number of constraints which are clauses	2072
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	29
Trace number 5893

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 02:27:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4376 boxname=wulflinc13 idbench=240 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1a86b94297136b91215b2ae8a8f5643  /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-4pb.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-4pb.opb /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-4pb.opb
IDLAUNCH: 4376
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        893708 kB
Buffers:         35308 kB
Cached:          85884 kB
SwapCached:        392 kB
Active:          54668 kB
Inactive:        69732 kB
HighTotal:      131008 kB
HighFree:        41272 kB
LowTotal:       903652 kB
LowFree:        852436 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10956 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:32:49 (client local time) WITH STATUS 30 IN 325.14 SECONDS
stats: 4376 0 325.14 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2096 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2082]---> BDD-cost:    1
c ---[2056]---> BDD-cost:    1
c ---[2034]---> BDD-cost:    1
c ---[2024]---> BDD-cost:    1
c ---[2022]---> BDD-cost:    1
c ---[1996]---> BDD-cost:    1
c ---[1978]---> BDD-cost:    1
c ---[1952]---> BDD-cost:    1
c ---[1950]---> BDD-cost:    1
c ---[1924]---> BDD-cost:    1
c ---[1906]---> BDD-cost:    1
c ---[1880]---> BDD-cost:    1
c ---[1866]---> BDD-cost:    1
c ---[1840]---> BDD-cost:    1
c ---[1818]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1736]---> BDD-cost:    1
c ---[1699]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1663]---> BDD-cost:    1
c ---[1637]---> BDD-cost:    1
c ---[1619]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1557]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1529]---> BDD-cost:    1
c ---[1523]---> BDD-cost:    1
c ---[1474]---> BDD-cost:    1
c ---[1464]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    1
c ---[1428]---> BDD-cost:    1
c ---[1390]---> BDD-cost:    1
c ---[1380]---> BDD-cost:    1
c ---[1378]---> BDD-cost:    1
c ---[1352]---> BDD-cost:    1
c ---[1334]---> BDD-cost:    1
c ---[1309]---> BDD-cost:    1
c ---[1291]---> BDD-cost:    1
c ---[1269]---> BDD-cost:    1
c ---[1243]---> BDD-cost:    1
c ---[1237]---> BDD-cost:    1
c ---[1235]---> BDD-cost:    1
c ---[1209]---> BDD-cost:    1
c ---[1191]---> BDD-cost:    1
c ---[1165]---> BDD-cost:    1
c ---[1112]---> BDD-cost:    1
c ---[1102]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1094]---> BDD-cost:    1
c ---[1057]---> BDD-cost:    1
c ---[1035]---> BDD-cost:    1
c ---[1029]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[ 991]---> BDD-cost:    1
c ---[ 965]---> BDD-cost:    1
c ---[ 963]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:    1
c ---[ 925]---> BDD-cost:    1
c ---[ 907]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 853]---> BDD-cost:    1
c ---[ 835]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 760]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 714]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:    1
c ---[ 571]---> BDD-cost:    1
c ---[ 533]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:    1
c ---[ 513]---> BDD-cost:    1
c ---[ 503]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:    1
c ---[ 414]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 386]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 370]---> BDD-cost:    1
c ---[ 360]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 298]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  103
c ---[  22]---> BDD-cost:  103
c ---[  21]---> BDD-cost:  103
c ---[  20]---> BDD-cost:  103
c ---[  19]---> BDD-cost:  103
c ---[  18]---> BDD-cost:  103
c ---[  17]---> BDD-cost:  103
c ---[  16]---> BDD-cost:  103
c ---[  15]---> BDD-cost:  103
c ---[  14]---> BDD-cost:  103
c ---[  13]---> BDD-cost:  103
c ---[  12]---> BDD-cost:  103
c ---[  11]---> BDD-cost:  103
c ---[  10]---> BDD-cost:  103
c ---[   9]---> BDD-cost:  103
c ---[   8]---> BDD-cost:  103
c ---[   7]---> BDD-cost:  103
c ---[   6]---> BDD-cost:  103
c ---[   5]---> BDD-cost:  103
c ---[   4]---> BDD-cost:  103
c ---[   3]---> BDD-cost:  103
c ---[   2]---> BDD-cost:  103
c ---[   1]---> BDD-cost:  103
c ---[   0]---> BDD-cost:  103
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8744    25274 |    2914       0        0     nan |  0.000 % |
c |       102 |    8744    25274 |    3205     102     1854    18.2 |  4.263 % |
c |       252 |    8744    25274 |    3525     252     8914    35.4 |  4.263 % |
c |       480 |    8744    25274 |    3878     480    16252    33.9 |  4.263 % |
c |       818 |    8744    25274 |    4266     818    27632    33.8 |  4.263 % |
c |      1330 |    8744    25274 |    4693    1330    40079    30.1 |  4.263 % |
c |      2092 |    8744    25274 |    5162    2092    66220    31.7 |  4.263 % |
c |      3234 |    8744    25274 |    5678    3234   112659    34.8 |  4.263 % |
c |      4947 |    8744    25274 |    6246    4947   200492    40.5 |  4.263 % |
c |      7511 |    8744    25274 |    6871    4053   147677    36.4 |  4.263 % |
c |     11355 |    8744    25274 |    7558    4314   120608    28.0 |  4.263 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:31844     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16770 |   45551   111127 |   15183    5795   193248    33.3 |  4.263 % |
c |     16870 |   45551   111127 |   16701    5895   196033    33.3 |  0.554 % |
c |     17020 |   45551   111127 |   18371    6045   200593    33.2 |  0.554 % |
c |     17246 |   45551   111127 |   20208    6271   207325    33.1 |  0.554 % |
c |     17584 |   45551   111127 |   22229    6609   218144    33.0 |  0.554 % |
c |     18090 |   45551   111127 |   24452    7115   233458    32.8 |  0.554 % |
c |     18850 |   45551   111127 |   26897    7875   260928    33.1 |  0.554 % |
c |     19989 |   45551   111127 |   29587    9014   303975    33.7 |  0.554 % |
c |     21698 |   45551   111127 |   32546   10723   364355    34.0 |  0.554 % |
c |     24260 |   45539   111103 |   35800   13284   454653    34.2 |  0.576 % |
c |     28104 |   45539   111103 |   39380   17128   569292    33.2 |  0.576 % |
c |     33870 |   45519   111063 |   43318   22892   762166    33.3 |  0.609 % |
c |     42519 |   45519   111063 |   47650   31541  1014782    32.2 |  0.609 % |
c |     55493 |   45494   111012 |   52415   44514  1375081    30.9 |  0.656 % |
c |     74956 |   45494   111012 |   57657   25926   619156    23.9 |  0.656 % |
c |    104148 |   45469   110961 |   63423   55117  1371941    24.9 |  0.703 % |
c |    147937 |   45425   110871 |   69765   51217  1026070    20.0 |  0.787 % |
c ==============================================================================
c [1mFound solution: 68[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 |    162691 |   45251   110490 |   15083   65969  1325224    20.1 |  0.787 % |
c |    162794 |   45251   110490 |   16591    8596   150390    17.5 |  1.268 % |
c |    162945 |   45251   110490 |   18250    8747   153049    17.5 |  1.268 % |
c |    163171 |   45251   110490 |   20075    8973   158495    17.7 |  1.268 % |
c |    163509 |   45251   110490 |   22083    9311   165961    17.8 |  1.268 % |
c |    164018 |   45251   110490 |   24291    9820   177554    18.1 |  1.268 % |
c |    164777 |   45251   110490 |   26720   10579   194824    18.4 |  1.268 % |
c |    165917 |   45251   110490 |   29392   11719   225785    19.3 |  1.268 % |
c |    167625 |   45107   110183 |   32331   13424   256721    19.1 |  1.559 % |
c |    170187 |   45062   110088 |   35564   15985   311087    19.5 |  1.639 % |
c |    174032 |   45062   110088 |   39121   19830   393033    19.8 |  1.639 % |
c |    179798 |   45062   110088 |   43033   25596   497332    19.4 |  1.639 % |
c |    188447 |   45062   110088 |   47336   34245   694865    20.3 |  1.639 % |
c ==============================================================================
c [1mFound solution: 66[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 |    189825 |   45062   110090 |   15020   35623   718705    20.2 |  1.639 % |
c |    189925 |   44941   109835 |   16522   14357   276516    19.3 |  1.930 % |
c |    190080 |   44941   109835 |   18174   14512   279937    19.3 |  1.930 % |
c |    190305 |   44941   109835 |   19991   14737   284880    19.3 |  1.930 % |
c |    190642 |   44802   109541 |   21990   15070   291877    19.4 |  2.196 % |
c ==============================================================================
c [1mFound solution: 64[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 |    191120 |   44421   108654 |   14807   15548   314191    20.2 |  2.196 % |
c |    191220 |   44421   108654 |   16287   15648   318112    20.3 |  3.210 % |
c |    191371 |   44331   108462 |   17916   15792   323356    20.5 |  3.381 % |
c |    191598 |   44331   108462 |   19708   16019   327914    20.5 |  3.381 % |
c |    191935 |   44331   108462 |   21678   16356   334846    20.5 |  3.381 % |
c |    192443 |   44331   108462 |   23846   16864   347077    20.6 |  3.381 % |
c |    193204 |   44331   108462 |   26231   17625   362351    20.6 |  3.381 % |
c |    194343 |   44225   108234 |   28854   18759   388671    20.7 |  3.588 % |
c |    196052 |   44113   107994 |   31740   20456   426188    20.8 |  3.799 % |
c |    198614 |   43964   107671 |   34914   23013   484185    21.0 |  4.098 % |
c |    202459 |   43964   107671 |   38405   26858   551368    20.5 |  4.098 % |
c ==============================================================================
c [1mFound solution: 62[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 |    203064 |   43962   107664 |   14654   27463   562617    20.5 |  4.098 % |
c |    203165 |   43962   107664 |   16119   13833   248851    18.0 |  4.168 % |
c |    203315 |   43962   107664 |   17731   13983   252059    18.0 |  4.168 % |
c |    203540 |   43893   107521 |   19504   14205   258006    18.2 |  4.292 % |
c |    203877 |   43893   107521 |   21454   14542   265507    18.3 |  4.292 % |
c |    204383 |   43865   107460 |   23600   15047   275133    18.3 |  4.350 % |
c |    205142 |   43865   107460 |   25960   15806   288978    18.3 |  4.350 % |
c |    206281 |   43788   107291 |   28556   16939   312056    18.4 |  4.507 % |
c |    207989 |   43732   107173 |   31412   18644   347555    18.6 |  4.609 % |
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 |    209269 |   43594   106848 |   14531   19906   372723    18.7 |  4.609 % |
c |    209369 |   43594   106848 |   15984   10053   172758    17.2 |  5.021 % |
c |    209522 |   43554   106760 |   17582   10204   174881    17.1 |  5.097 % |
c |    209749 |   43467   106570 |   19340   10422   178532    17.1 |  5.272 % |
c |    210086 |   43270   106132 |   21274   10744   182597    17.0 |  5.690 % |
c ==============================================================================
c [1mOptimal solution: 60[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
c _______________________________________________________________________________
c 
c restarts              : 71
c conflicts             : 210539         (648 /sec)
c decisions             : 317098         (976 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 324.844 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.90 0.95 0.91 2/54 5037
Raw data (stat): 5037 (runsolver) R 5036 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422768416 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 3023 0 0 0 990 8 0 0 25 0 1 0 422768416 14708736 2935 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3591 2935 603 41 0 3550 0
vsize: 14364
[startup+20.0015 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 3576 0 0 0 1988 10 0 0 25 0 1 0 422768416 17051648 3488 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4163 3488 603 41 0 4122 0
vsize: 16652
[startup+30.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 3934 0 0 0 2986 12 0 0 25 0 1 0 422768416 18661376 3846 4294967295 134512640 134672761 3221224560 3221223744 134558916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4556 3846 603 41 0 4515 0
vsize: 18224
[startup+40.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4228 0 0 0 3984 14 0 0 25 0 1 0 422768416 19894272 4140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4857 4140 603 41 0 4816 0
vsize: 19428
[startup+50.0035 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4446 0 0 0 4983 15 0 0 25 0 1 0 422768416 20738048 4358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5063 4358 603 41 0 5022 0
vsize: 20252
[startup+60.0042 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4618 0 0 0 5982 16 0 0 25 0 1 0 422768416 21487616 4530 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5246 4530 603 41 0 5205 0
vsize: 20984
[startup+70.0043 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4637 0 0 0 6981 17 0 0 25 0 1 0 422768416 21626880 4549 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5280 4549 603 41 0 5239 0
vsize: 21120
[startup+80.0055 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4669 0 0 0 7981 17 0 0 25 0 1 0 422768416 21790720 4581 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5320 4581 603 41 0 5279 0
vsize: 21280
[startup+90.0061 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4694 0 0 0 8980 18 0 0 25 0 1 0 422768416 21987328 4606 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4606 603 41 0 5327 0
vsize: 21472
[startup+100.006 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4727 0 0 0 9980 18 0 0 25 0 1 0 422768416 22151168 4639 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5408 4639 603 41 0 5367 0
vsize: 21632
[startup+110.007 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4749 0 0 0 10980 19 0 0 25 0 1 0 422768416 22151168 4661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5408 4661 603 41 0 5367 0
vsize: 21632
[startup+120.008 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4773 0 0 0 11979 19 0 0 25 0 1 0 422768416 22347776 4685 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5456 4685 603 41 0 5415 0
vsize: 21824
[startup+130.007 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4801 0 0 0 12978 19 0 0 25 0 1 0 422768416 22347776 4713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5456 4713 603 41 0 5415 0
vsize: 21824
[startup+140.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4872 0 0 0 13978 20 0 0 25 0 1 0 422768416 22724608 4784 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5548 4784 603 41 0 5507 0
vsize: 22192
[startup+150.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4882 0 0 0 14978 20 0 0 25 0 1 0 422768416 22724608 4794 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5548 4794 603 41 0 5507 0
vsize: 22192
[startup+160.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4907 0 0 0 15977 21 0 0 25 0 1 0 422768416 22859776 4819 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 4819 603 41 0 5540 0
vsize: 22324
[startup+170.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4910 0 0 0 16977 21 0 0 25 0 1 0 422768416 22859776 4822 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 4822 603 41 0 5540 0
vsize: 22324
[startup+180.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4948 0 0 0 17977 21 0 0 25 0 1 0 422768416 23056384 4860 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5629 4860 603 41 0 5588 0
vsize: 22516
[startup+190.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4951 0 0 0 18976 22 0 0 25 0 1 0 422768416 23056384 4863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5629 4863 603 41 0 5588 0
vsize: 22516
[startup+200.012 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4954 0 0 0 19976 22 0 0 25 0 1 0 422768416 23056384 4866 4294967295 134512640 134672761 3221224560 3221223728 134553603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5629 4866 603 41 0 5588 0
vsize: 22516
[startup+210.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 4956 0 0 0 20975 23 0 0 25 0 1 0 422768416 23056384 4868 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5629 4868 603 41 0 5588 0
vsize: 22516
[startup+220.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5050 0 0 0 21975 23 0 0 25 0 1 0 422768416 23515136 4962 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5741 4962 603 41 0 5700 0
vsize: 22964
[startup+230.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5053 0 0 0 22975 23 0 0 25 0 1 0 422768416 23515136 4965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5741 4965 603 41 0 5700 0
vsize: 22964
[startup+240.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5055 0 0 0 23974 24 0 0 25 0 1 0 422768416 23515136 4967 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5741 4967 603 41 0 5700 0
vsize: 22964
[startup+250.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5098 0 0 0 24974 24 0 0 25 0 1 0 422768416 23990272 5010 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5010 603 41 0 5816 0
vsize: 23428
[startup+260.017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5098 0 0 0 25974 24 0 0 25 0 1 0 422768416 23990272 5010 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5010 603 41 0 5816 0
vsize: 23428
[startup+270.018 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5098 0 0 0 26973 25 0 0 25 0 1 0 422768416 23990272 5010 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5010 603 41 0 5816 0
vsize: 23428
[startup+280.018 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5100 0 0 0 27973 25 0 0 25 0 1 0 422768416 23990272 5012 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5012 603 41 0 5816 0
vsize: 23428
[startup+290.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5100 0 0 0 28973 25 0 0 25 0 1 0 422768416 23990272 5012 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5012 603 41 0 5816 0
vsize: 23428
[startup+300.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5101 0 0 0 29972 26 0 0 25 0 1 0 422768416 23990272 5013 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5013 603 41 0 5816 0
vsize: 23428
[startup+310.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5101 0 0 0 30972 26 0 0 25 0 1 0 422768416 23990272 5013 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5013 603 41 0 5816 0
vsize: 23428
[startup+320.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5101 0 0 0 31972 26 0 0 25 0 1 0 422768416 23990272 5013 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5013 603 41 0 5816 0
vsize: 23428
[startup+325.172 s]
Raw data (loadavg): 1.00 0.97 0.92 1/53 5037
Raw data (stat): 5037 (minisat+) R 5036 30701 30700 0 -1 0 5101 0 0 0 31972 26 0 0 25 0 1 0 422768416 23990272 5013 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5013 603 41 0 5816 0
vsize: 0

Child status: 30
Real time (s): 325.172
CPU time (s): 325.14
CPU user time (s): 324.857
CPU system time (s): 0.282956
CPU usage (%): 99.99
Max. virtual memory (Kb): 23428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####