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 4939

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 21:10:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2156 boxname=wulflinc13 idbench=240 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c1a86b94297136b91215b2ae8a8f5643  /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-4pb.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-s4-4-3-4pb.opb
IDLAUNCH: 2156
/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:        924252 kB
Buffers:         34052 kB
Cached:          56880 kB
SwapCached:        392 kB
Active:          50504 kB
Inactive:        43644 kB
HighTotal:      131008 kB
HighFree:        70224 kB
LowTotal:       903652 kB
LowFree:        854028 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10676 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:15:52 (client local time) WITH STATUS 30 IN 329.187 SECONDS
stats: 2156 0 329.187 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         (640 /sec)
c decisions             : 317098         (964 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 329.011 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.92 2/54 1295
Raw data (stat): 1295 (runsolver) D 1294 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420866100 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 3030 0 0 0 991 6 0 0 25 0 1 0 420866100 14757888 2943 4294967295 134512640 134672761 3221224624 3221223692 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3603 2943 603 41 0 3562 0
vsize: 14412
[startup+19.9998 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 3582 0 0 0 1988 9 0 0 25 0 1 0 420866100 16973824 3495 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4144 3495 603 41 0 4103 0
vsize: 16576
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 3938 0 0 0 2986 10 0 0 25 0 1 0 420866100 18710528 3851 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4568 3851 603 41 0 4527 0
vsize: 18272
[startup+40 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4230 0 0 0 3986 11 0 0 25 0 1 0 420866100 19804160 4143 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4835 4143 603 41 0 4794 0
vsize: 19340
[startup+50.0007 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4447 0 0 0 4985 12 0 0 25 0 1 0 420866100 20787200 4360 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5075 4360 603 41 0 5034 0
vsize: 20300
[startup+60.0003 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4630 0 0 0 5985 12 0 0 25 0 1 0 420866100 21536768 4543 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5258 4543 603 41 0 5217 0
vsize: 21032
[startup+70.0003 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4650 0 0 0 6985 12 0 0 25 0 1 0 420866100 21676032 4563 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5292 4563 603 41 0 5251 0
vsize: 21168
[startup+80.0007 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4679 0 0 0 7985 13 0 0 25 0 1 0 420866100 21839872 4592 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5332 4592 603 41 0 5291 0
vsize: 21328
[startup+90.0003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4706 0 0 0 8985 13 0 0 25 0 1 0 420866100 22036480 4619 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5380 4619 603 41 0 5339 0
vsize: 21520
[startup+100 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4739 0 0 0 9985 13 0 0 25 0 1 0 420866100 22200320 4652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5420 4652 603 41 0 5379 0
vsize: 21680
[startup+110.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4761 0 0 0 10985 13 0 0 25 0 1 0 420866100 22200320 4674 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5420 4674 603 41 0 5379 0
vsize: 21680
[startup+120 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4782 0 0 0 11985 13 0 0 25 0 1 0 420866100 22396928 4695 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5468 4695 603 41 0 5427 0
vsize: 21872
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4811 0 0 0 12985 13 0 0 25 0 1 0 420866100 22396928 4724 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5468 4724 603 41 0 5427 0
vsize: 21872
[startup+140 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4885 0 0 0 13985 13 0 0 25 0 1 0 420866100 22773760 4798 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5560 4798 603 41 0 5519 0
vsize: 22240
[startup+150 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4895 0 0 0 14986 13 0 0 25 0 1 0 420866100 22773760 4808 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5560 4808 603 41 0 5519 0
vsize: 22240
[startup+160 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4920 0 0 0 15986 13 0 0 25 0 1 0 420866100 22908928 4833 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5593 4833 603 41 0 5552 0
vsize: 22372
[startup+170 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4923 0 0 0 16986 13 0 0 25 0 1 0 420866100 22908928 4836 4294967295 134512640 134672761 3221224624 3221223748 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5593 4836 603 41 0 5552 0
vsize: 22372
[startup+179.999 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4960 0 0 0 17986 14 0 0 25 0 1 0 420866100 23105536 4873 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5641 4873 603 41 0 5600 0
vsize: 22564
[startup+189.999 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4965 0 0 0 18986 14 0 0 25 0 1 0 420866100 23105536 4878 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5641 4878 603 41 0 5600 0
vsize: 22564
[startup+200 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4968 0 0 0 19986 14 0 0 25 0 1 0 420866100 23105536 4881 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5641 4881 603 41 0 5600 0
vsize: 22564
[startup+209.999 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 4971 0 0 0 20986 14 0 0 25 0 1 0 420866100 23105536 4884 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5641 4884 603 41 0 5600 0
vsize: 22564
[startup+219.999 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5062 0 0 0 21986 14 0 0 25 0 1 0 420866100 23564288 4975 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5753 4975 603 41 0 5712 0
vsize: 23012
[startup+230 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5068 0 0 0 22986 14 0 0 25 0 1 0 420866100 23564288 4981 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5753 4981 603 41 0 5712 0
vsize: 23012
[startup+239.999 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5069 0 0 0 23986 14 0 0 25 0 1 0 420866100 23564288 4982 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5753 4982 603 41 0 5712 0
vsize: 23012
[startup+250 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5121 0 0 0 24986 14 0 0 25 0 1 0 420866100 24039424 5034 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5034 603 41 0 5828 0
vsize: 23476
[startup+260.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5121 0 0 0 25986 14 0 0 25 0 1 0 420866100 24039424 5034 4294967295 134512640 134672761 3221224624 3221223728 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5034 603 41 0 5828 0
vsize: 23476
[startup+270 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5121 0 0 0 26986 14 0 0 25 0 1 0 420866100 24039424 5034 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5034 603 41 0 5828 0
vsize: 23476
[startup+280 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5123 0 0 0 27987 14 0 0 25 0 1 0 420866100 24039424 5036 4294967295 134512640 134672761 3221224624 3221223824 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5036 603 41 0 5828 0
vsize: 23476
[startup+290.001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5123 0 0 0 28987 14 0 0 25 0 1 0 420866100 24039424 5036 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5036 603 41 0 5828 0
vsize: 23476
[startup+300 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5124 0 0 0 29987 14 0 0 25 0 1 0 420866100 24039424 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5037 603 41 0 5828 0
vsize: 23476
[startup+310 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5124 0 0 0 30987 14 0 0 25 0 1 0 420866100 24039424 5037 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5037 603 41 0 5828 0
vsize: 23476
[startup+320 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5124 0 0 0 31987 14 0 0 25 0 1 0 420866100 24039424 5037 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5037 603 41 0 5828 0
vsize: 23476
[startup+329.161 s]
Raw data (loadavg): 0.99 0.98 0.92 1/53 1295
Raw data (stat): 1295 (minisat+) R 1294 30701 30700 0 -1 0 5124 0 0 0 31987 14 0 0 25 0 1 0 420866100 24039424 5037 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5869 5037 603 41 0 5828 0
vsize: 0

Child status: 30
Real time (s): 329.161
CPU time (s): 329.187
CPU user time (s): 329.026
CPU system time (s): 0.160975
CPU usage (%): 100.008
Max. virtual memory (Kb): 23476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####