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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namesubmitted/manquinho/routing/normalized-s4-4-3-4pb.opb
MD5SUMc1a86b94297136b91215b2ae8a8f5643
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 60
Optimality of the best value was proved YES
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 numbers10
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark157.286
Number of variables696
Total number of constraints2096
Number of constraints which are clauses2072
Number of constraints which are cardinality constraints (but not clauses)24
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint29

Trace number 2174

Launcher Data

LAUNCH ON wulflinc1 THE 2005-09-18 18:07:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2583 boxname=wulflinc1 idbench=239 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1a86b94297136b91215b2ae8a8f5643  /oldhome/oroussel/tmp/wulflinc1/normalized-s4-4-3-4pb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-s4-4-3-4pb.opb
IDLAUNCH: 2583
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        882624 kB
Buffers:         37860 kB
Cached:          84448 kB
SwapCached:        908 kB
Active:          95132 kB
Inactive:        30040 kB
HighTotal:      131008 kB
HighFree:        50484 kB
LowTotal:       903652 kB
LowFree:        832140 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21168 kB
Committed_AS:    93168 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:13:01 (client local time) WITH STATUS 30 IN 328.427 SECONDS
stats: 2583 0 328.427 30

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 Found solution: 70
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 Found solution: 68
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 Found solution: 66
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 Found solution: 64
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 Found solution: 62
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 Found solution: 60
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 Optimal solution: 60
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         (642 /sec)
c decisions             : 317098         (966 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 328.108 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/26780/stat): 26780 (minisat+_script) R 26779 26780 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1728207679 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26780/statm): 174 3 169 147 0 27 0
[pid=26780] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=26781
New process pid=26782
New process pid=26783
execve syscall for /bin/sed executable
One traced child (pid=26782) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=26783) exited with status: 0
One traced child (pid=26781) exited with status: 0
New process pid=26784
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-s4-4-3-4pb.opb

[startup+10.0039 s]
Raw data (loadavg): 0.93 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 2904 0 0 0 970 12 0 0 25 0 1 0 1728207684 12734464 2762 4294967295 134512640 135094434 3221224448 3221223040 134551879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 3109 2762 145 145 0 2964 0
[pid=26784] vsize: 12436
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 14560

[startup+20.0047 s]
Raw data (loadavg): 0.94 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 3468 0 0 0 1960 16 0 0 25 0 1 0 1728207684 15073280 3326 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 3680 3326 145 145 0 3535 0
[pid=26784] vsize: 14720
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 16844

[startup+30.0055 s]
Raw data (loadavg): 0.95 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 3829 0 0 0 2955 19 0 0 25 0 1 0 1728207684 16695296 3687 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 4076 3687 145 145 0 3931 0
[pid=26784] vsize: 16304
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 18428

[startup+40.0063 s]
Raw data (loadavg): 0.96 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4128 0 0 0 3950 21 0 0 25 0 1 0 1728207684 17920000 3986 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 4375 3986 145 145 0 4230 0
[pid=26784] vsize: 17500
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 19624

[startup+50.0071 s]
Raw data (loadavg): 0.96 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4344 0 0 0 4946 23 0 0 25 0 1 0 1728207684 18853888 4202 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 4603 4202 145 145 0 4458 0
[pid=26784] vsize: 18412
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 20536

[startup+60.0078 s]
Raw data (loadavg): 0.97 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4535 0 0 0 5943 24 0 0 25 0 1 0 1728207684 19664896 4393 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 4801 4393 145 145 0 4656 0
[pid=26784] vsize: 19204
Current children cumulated CPU time (s) 59.67
Current children cumulated vsize (Kb) 21328

[startup+70.0086 s]
Raw data (loadavg): 0.97 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4555 0 0 0 6943 24 0 0 25 0 1 0 1728207684 19746816 4413 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 4821 4413 145 145 0 4676 0
[pid=26784] vsize: 19284
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 21408

[startup+80.0094 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4584 0 0 0 7943 24 0 0 25 0 1 0 1728207684 19877888 4442 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 4853 4442 145 145 0 4708 0
[pid=26784] vsize: 19412
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 21536

[startup+90.0101 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4611 0 0 0 8943 24 0 0 25 0 1 0 1728207684 20140032 4469 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 4917 4469 145 145 0 4772 0
[pid=26784] vsize: 19668
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 21792

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4645 0 0 0 9943 24 0 0 25 0 1 0 1728207684 20303872 4503 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 4957 4503 145 145 0 4812 0
[pid=26784] vsize: 19828
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 21952

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4667 0 0 0 10943 24 0 0 25 0 1 0 1728207684 20336640 4525 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 4965 4525 145 145 0 4820 0
[pid=26784] vsize: 19860
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 21984

[startup+120.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4688 0 0 0 11943 24 0 0 25 0 1 0 1728207684 20434944 4546 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 4989 4546 145 145 0 4844 0
[pid=26784] vsize: 19956
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 22080

[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4717 0 0 0 12943 25 0 0 25 0 1 0 1728207684 20500480 4575 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5005 4575 145 145 0 4860 0
[pid=26784] vsize: 20020
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 22144

[startup+140.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4789 0 0 0 13943 25 0 0 25 0 1 0 1728207684 20811776 4647 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5081 4647 145 145 0 4936 0
[pid=26784] vsize: 20324
Current children cumulated CPU time (s) 139.68
Current children cumulated vsize (Kb) 22448

[startup+150.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4799 0 0 0 14943 25 0 0 25 0 1 0 1728207684 20877312 4657 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5097 4657 145 145 0 4952 0
[pid=26784] vsize: 20388
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 22512

[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4824 0 0 0 15943 25 0 0 25 0 1 0 1728207684 21008384 4682 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5129 4682 145 145 0 4984 0
[pid=26784] vsize: 20516
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 22640

[startup+170.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4827 0 0 0 16944 25 0 0 25 0 1 0 1728207684 21008384 4685 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5129 4685 145 145 0 4984 0
[pid=26784] vsize: 20516
Current children cumulated CPU time (s) 169.69
Current children cumulated vsize (Kb) 22640

[startup+180.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4864 0 0 0 17944 25 0 0 25 0 1 0 1728207684 21204992 4722 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5177 4722 145 145 0 5032 0
[pid=26784] vsize: 20708
Current children cumulated CPU time (s) 179.69
Current children cumulated vsize (Kb) 22832

[startup+190.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4868 0 0 0 18944 25 0 0 25 0 1 0 1728207684 21204992 4726 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5177 4726 145 145 0 5032 0
[pid=26784] vsize: 20708
Current children cumulated CPU time (s) 189.69
Current children cumulated vsize (Kb) 22832

[startup+200.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4871 0 0 0 19944 25 0 0 25 0 1 0 1728207684 21204992 4729 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 5177 4729 145 145 0 5032 0
[pid=26784] vsize: 20708
Current children cumulated CPU time (s) 199.69
Current children cumulated vsize (Kb) 22832

[startup+210.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4873 0 0 0 20943 26 0 0 25 0 1 0 1728207684 21204992 4731 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26784/statm): 5177 4731 145 145 0 5032 0
[pid=26784] vsize: 20708
Current children cumulated CPU time (s) 209.69
Current children cumulated vsize (Kb) 22832

[startup+220.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4966 0 0 0 21943 26 0 0 25 0 1 0 1728207684 21598208 4792 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5273 4792 145 145 0 5128 0
[pid=26784] vsize: 21092
Current children cumulated CPU time (s) 219.69
Current children cumulated vsize (Kb) 23216

[startup+230.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4969 0 0 0 22943 26 0 0 25 0 1 0 1728207684 21598208 4795 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5273 4795 145 145 0 5128 0
[pid=26784] vsize: 21092
Current children cumulated CPU time (s) 229.69
Current children cumulated vsize (Kb) 23216

[startup+240.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 4970 0 0 0 23943 26 0 0 25 0 1 0 1728207684 21598208 4796 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5273 4796 145 145 0 5128 0
[pid=26784] vsize: 21092
Current children cumulated CPU time (s) 239.69
Current children cumulated vsize (Kb) 23216

[startup+250.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5022 0 0 0 24943 26 0 0 25 0 1 0 1728207684 22073344 4848 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4848 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 249.69
Current children cumulated vsize (Kb) 23680

[startup+260.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5022 0 0 0 25943 26 0 0 25 0 1 0 1728207684 22073344 4848 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4848 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 259.69
Current children cumulated vsize (Kb) 23680

[startup+270.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5022 0 0 0 26943 26 0 0 25 0 1 0 1728207684 22073344 4848 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4848 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 269.69
Current children cumulated vsize (Kb) 23680

[startup+280.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5024 0 0 0 27944 26 0 0 25 0 1 0 1728207684 22073344 4850 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4850 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 279.7
Current children cumulated vsize (Kb) 23680

[startup+290.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5024 0 0 0 28944 26 0 0 25 0 1 0 1728207684 22073344 4850 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4850 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 289.7
Current children cumulated vsize (Kb) 23680

[startup+300.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5025 0 0 0 29944 26 0 0 25 0 1 0 1728207684 22073344 4851 4294967295 134512640 135094434 3221224448 3221223040 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4851 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 299.7
Current children cumulated vsize (Kb) 23680

[startup+310.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5025 0 0 0 30944 26 0 0 25 0 1 0 1728207684 22073344 4851 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4851 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 309.7
Current children cumulated vsize (Kb) 23680

[startup+320.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 26784
Raw data (/proc/26780/stat): 26780 (minisat+_script) S 26779 26780 17733 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1728207679 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26780/statm): 531 226 485 147 0 384 0
[pid=26780] vsize: 2124
Raw data (/proc/26784/stat): 26784 (minisat+_64-bit) R 26780 26780 17733 0 -1 0 5025 0 0 0 31944 26 0 0 25 0 1 0 1728207684 22073344 4851 4294967295 134512640 135094434 3221224448 3221223152 134559013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26784/statm): 5389 4851 145 145 0 5244 0
[pid=26784] vsize: 21556
Current children cumulated CPU time (s) 319.7
Current children cumulated vsize (Kb) 23680
One traced child (pid=26784) exited with status: 30
One traced child (pid=26780) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 328.717
CPU time (s): 328.427
CPU user time (s): 328.127
CPU system time (s): 0.299954
CPU usage (%): 99.9117
Max. virtual memory (cumulated for all children) (Kb): 23680

Verifier Data

Verifier:	OK	60