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 6277

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        818264 kB
Buffers:         36368 kB
Cached:         145128 kB
SwapCached:       2376 kB
Active:          59652 kB
Inactive:       127244 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        818012 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23640 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:27:32 (client local time) WITH STATUS 30 IN 470.047 SECONDS
stats: 4752 0 470.047 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 |   14816    43346 |    4938       0        0     nan |  0.000 % |
c |       100 |   14816    43346 |    5431     100     1608    16.1 |  4.263 % |
c |       251 |   14816    43346 |    5974     251     5971    23.8 |  4.263 % |
c |       476 |   14816    43346 |    6572     476    12946    27.2 |  4.263 % |
c |       815 |   14816    43346 |    7229     815    28156    34.5 |  4.263 % |
c ==============================================================================
c [1mFound solution: 72[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 |      1061 |   86261   210667 |   28753    1061    33819    31.9 |  4.263 % |
c |      1161 |   86261   210667 |   31628    1161    35797    30.8 |  2.506 % |
c |      1311 |   86261   210667 |   34791    1311    38389    29.3 |  2.506 % |
c |      1537 |   86072   210243 |   38270    1531    40350    26.4 |  2.692 % |
c |      1874 |   85838   209714 |   42097    1862    43186    23.2 |  2.928 % |
c |      2383 |   85711   209425 |   46306    2369    53133    22.4 |  3.059 % |
c |      3145 |   85711   209425 |   50937    3131    83778    26.8 |  3.059 % |
c |      4288 |   85711   209425 |   56031    4274   124357    29.1 |  3.059 % |
c |      5997 |   85711   209425 |   61634    5983   208527    34.9 |  3.059 % |
c |      8559 |   85072   207972 |   67798    8407   310945    37.0 |  3.707 % |
c |     12403 |   80950   198546 |   74577   12217   415505    34.0 |  8.167 % |
c |     18170 |   78509   192910 |   82035   17888   536516    30.0 | 10.771 % |
c |     26825 |   73669   181640 |   90239   26139   745662    28.5 | 15.951 % |
c |     39799 |   66338   164601 |   99263   38467  1073589    27.9 | 24.100 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:28576     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40074 |  128629   310168 |   42876   38693  1079748    27.9 | 24.100 % |
c |     40174 |  128570   310037 |   47163   38792  1080530    27.9 | 14.842 % |
c |     40324 |  128570   310037 |   51879   38942  1083299    27.8 | 14.842 % |
c |     40551 |  128570   310037 |   57067   39169  1088699    27.8 | 14.842 % |
c |     40888 |  128570   310037 |   62774   39506  1096967    27.8 | 14.842 % |
c |     41394 |  127724   308142 |   69052   39959  1102797    27.6 | 15.355 % |
c |     42153 |  127624   307909 |   75957   40703  1131309    27.8 | 15.425 % |
c |     43295 |  127168   306802 |   83553   41818  1167460    27.9 | 15.691 % |
c |     45003 |  127168   306802 |   91908   43526  1213954    27.9 | 15.691 % |
c |     47566 |  127168   306802 |  101099   46089  1284371    27.9 | 15.691 % |
c |     51411 |  127137   306709 |  111209   49933  1374256    27.5 | 15.704 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:25604     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53247 |  181287   433360 |   60429   51769  1430738    27.6 | 15.704 % |
c |     53349 |  181287   433360 |   66471   51871  1431828    27.6 | 11.974 % |
c |     53500 |  181287   433360 |   73119   52022  1435239    27.6 | 11.974 % |
c |     53725 |  181287   433360 |   80430   52247  1444579    27.6 | 11.974 % |
c |     54063 |  181287   433360 |   88474   52585  1452392    27.6 | 11.974 % |
c |     54569 |  181287   433360 |   97321   53091  1468855    27.7 | 11.974 % |
c |     55328 |  181287   433360 |  107053   53850  1492991    27.7 | 11.974 % |
c |     56471 |  180475   431510 |  117759   54968  1515276    27.6 | 12.323 % |
c |     58182 |  180106   430682 |  129534   56675  1564837    27.6 | 12.475 % |
c |     60745 |  180031   430515 |  142488   59237  1637292    27.6 | 12.506 % |
c |     64589 |  179273   428751 |  156737   63011  1774131    28.2 | 12.820 % |
c |     70358 |  176847   423194 |  172410   68612  1926516    28.1 | 13.948 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:18058     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77330 |  204337   487900 |   68112   75395  2142832    28.4 | 13.948 % |
c |     77430 |  204337   487900 |   74923   75495  2144786    28.4 | 14.122 % |
c |     77580 |  204337   487900 |   82415   75645  2147837    28.4 | 14.122 % |
c |     77805 |  204337   487900 |   90657   75870  2154316    28.4 | 14.122 % |
c |     78144 |  204337   487900 |   99722   76209  2161793    28.4 | 14.122 % |
c |     78650 |  204337   487900 |  109695   76715  2175121    28.4 | 14.122 % |
c |     79411 |  203789   486650 |  120664   77464  2204718    28.5 | 14.334 % |
c |     80552 |  203381   485726 |  132731   78598  2244914    28.6 | 14.478 % |
c |     82263 |  201370   481149 |  146004   80280  2297002    28.6 | 15.226 % |
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 |     82553 |  201372   481156 |   67124   80570  2307589    28.6 | 15.226 % |
c |     82654 |  201295   480980 |   73836   22303   488596    21.9 | 15.264 % |
c |     82805 |  201295   480980 |   81220   22454   492439    21.9 | 15.264 % |
c |     83030 |  201295   480980 |   89342   22679   498022    22.0 | 15.265 % |
c |     83368 |  201224   480818 |   98276   23014   505586    22.0 | 15.290 % |
c |     83874 |  201224   480818 |  108103   23520   521400    22.2 | 15.290 % |
c |     84634 |  201175   480704 |  118914   24278   542174    22.3 | 15.307 % |
c |     85773 |  201175   480704 |  130805   25417   576717    22.7 | 15.307 % |
c |     87482 |  201175   480704 |  143886   27126   611393    22.5 | 15.307 % |
c |     90044 |  200291   478664 |  158274   29665   674159    22.7 | 15.631 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 8910     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93637 |  204613   489124 |   68204   33200   769623    23.2 | 15.631 % |
c |     93738 |  204613   489124 |   75024   33301   771584    23.2 | 17.176 % |
c |     93888 |  204613   489124 |   82526   33451   775177    23.2 | 17.176 % |
c |     94113 |  204613   489124 |   90779   33676   779428    23.1 | 17.176 % |
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 |     94231 |  204617   489140 |   68205   33794   782293    23.1 | 17.176 % |
c |     94334 |  204091   487934 |   75025   33864   781378    23.1 | 17.373 % |
c |     94485 |  203970   487649 |   82528   34011   784970    23.1 | 17.422 % |
c |     94710 |  203970   487649 |   90780   34236   789046    23.0 | 17.422 % |
c |     95049 |  203829   487309 |   99858   34573   794545    23.0 | 17.469 % |
c |     95557 |  194879   466713 |  109844   18933   332367    17.6 | 20.847 % |
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             : 95676          (204 /sec)
c decisions             : 178125         (379 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 469.687 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.89 0.91 0.90 2/55 29234
Raw data (stat): 29234 (runsolver) R 29233 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481667367 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0009 s]
Raw data (loadavg): 0.91 0.91 0.90 2/55 29234
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 2952 0 0 0 991 7 0 0 25 0 1 0 481667367 14467072 2875 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3532 2875 603 41 0 3491 0
vsize: 14128
[startup+20.002 s]
Raw data (loadavg): 0.92 0.92 0.91 2/55 29234
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 3227 0 0 0 1991 8 0 0 25 0 1 0 481667367 15540224 3150 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3794 3150 603 41 0 3753 0
vsize: 15176
[startup+30.0024 s]
Raw data (loadavg): 0.93 0.92 0.91 2/55 29234
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 3377 0 0 0 2990 8 0 0 25 0 1 0 481667367 16150528 3300 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3943 3300 603 41 0 3902 0
vsize: 15772
[startup+40.0035 s]
Raw data (loadavg): 0.94 0.92 0.91 2/55 29234
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 3588 0 0 0 3988 9 0 0 25 0 1 0 481667367 17088512 3511 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4172 3511 603 41 0 4131 0
vsize: 16688
[startup+50.0038 s]
Raw data (loadavg): 0.95 0.92 0.91 2/55 29234
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 3668 0 0 0 4987 10 0 0 25 0 1 0 481667367 17358848 3591 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4238 3591 603 41 0 4197 0
vsize: 16952
[startup+60.0031 s]
Raw data (loadavg): 0.96 0.92 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 3763 0 0 0 5987 10 0 0 25 0 1 0 481667367 17760256 3686 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4336 3686 603 41 0 4295 0
vsize: 17344
[startup+70.0042 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 3907 0 0 0 6987 10 0 0 25 0 1 0 481667367 18419712 3830 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4497 3830 603 41 0 4456 0
vsize: 17988
[startup+80.0043 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 4016 0 0 0 7987 10 0 0 25 0 1 0 481667367 18817024 3939 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4594 3939 603 41 0 4553 0
vsize: 18376
[startup+90.0052 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 5895 0 0 0 8983 15 0 0 25 0 1 0 481667367 26275840 5731 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5731 603 41 0 6374 0
vsize: 25660
[startup+100.005 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 5989 0 0 0 9983 15 0 0 25 0 1 0 481667367 26677248 5825 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6513 5825 603 41 0 6472 0
vsize: 26052
[startup+110.004 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 6067 0 0 0 10983 15 0 0 25 0 1 0 481667367 26943488 5903 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6578 5903 603 41 0 6537 0
vsize: 26312
[startup+120.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 6145 0 0 0 11983 15 0 0 25 0 1 0 481667367 27340800 5981 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6675 5981 603 41 0 6634 0
vsize: 26700
[startup+130.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 6210 0 0 0 12983 16 0 0 25 0 1 0 481667367 27475968 6046 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6708 6046 603 41 0 6667 0
vsize: 26832
[startup+140.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 6270 0 0 0 13983 16 0 0 25 0 1 0 481667367 27770880 6106 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6780 6106 603 41 0 6739 0
vsize: 27120
[startup+150.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8134 0 0 0 14979 19 0 0 25 0 1 0 481667367 38412288 7805 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9378 7805 603 41 0 9337 0
vsize: 37512
[startup+160.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8194 0 0 0 15979 20 0 0 25 0 1 0 481667367 38682624 7865 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9444 7865 603 41 0 9403 0
vsize: 37776
[startup+170.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8237 0 0 0 16979 20 0 0 25 0 1 0 481667367 38817792 7908 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9477 7908 603 41 0 9436 0
vsize: 37908
[startup+180.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8306 0 0 0 17978 21 0 0 25 0 1 0 481667367 39079936 7977 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9541 7977 603 41 0 9500 0
vsize: 38164
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8364 0 0 0 18977 21 0 0 25 0 1 0 481667367 39211008 8035 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9573 8035 603 41 0 9532 0
vsize: 38292
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8443 0 0 0 19977 21 0 0 25 0 1 0 481667367 39616512 8114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9672 8114 603 41 0 9631 0
vsize: 38688
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8507 0 0 0 20977 21 0 0 25 0 1 0 481667367 39882752 8178 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9737 8178 603 41 0 9696 0
vsize: 38948
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8573 0 0 0 21977 21 0 0 25 0 1 0 481667367 40148992 8244 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9802 8244 603 41 0 9761 0
vsize: 39208
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8639 0 0 0 22977 22 0 0 25 0 1 0 481667367 40484864 8310 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9884 8310 603 41 0 9843 0
vsize: 39536
[startup+240.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8690 0 0 0 23977 22 0 0 25 0 1 0 481667367 40882176 8361 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9981 8361 603 41 0 9940 0
vsize: 39924
[startup+250.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8737 0 0 0 24977 22 0 0 25 0 1 0 481667367 41181184 8408 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 8408 603 41 0 10013 0
vsize: 40216
[startup+260.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8784 0 0 0 25977 22 0 0 25 0 1 0 481667367 41312256 8455 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10086 8455 603 41 0 10045 0
vsize: 40344
[startup+270.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8839 0 0 0 26977 22 0 0 25 0 1 0 481667367 41459712 8510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10122 8510 603 41 0 10081 0
vsize: 40488
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8878 0 0 0 27977 23 0 0 25 0 1 0 481667367 41734144 8549 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10189 8549 603 41 0 10148 0
vsize: 40756
[startup+290.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8954 0 0 0 28977 23 0 0 25 0 1 0 481667367 42004480 8625 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10255 8625 603 41 0 10214 0
vsize: 41020
[startup+300.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 8988 0 0 0 29977 23 0 0 25 0 1 0 481667367 42164224 8659 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10294 8659 603 41 0 10253 0
vsize: 41176
[startup+310.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 9044 0 0 0 30977 23 0 0 25 0 1 0 481667367 42446848 8715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10363 8715 603 41 0 10322 0
vsize: 41452
[startup+320.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 9951 0 0 0 31975 26 0 0 25 0 1 0 481667367 45486080 9622 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11105 9622 603 41 0 11064 0
vsize: 44420
[startup+330.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10013 0 0 0 32975 26 0 0 25 0 1 0 481667367 45621248 9684 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11138 9684 603 41 0 11097 0
vsize: 44552
[startup+340.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10054 0 0 0 33975 26 0 0 25 0 1 0 481667367 45756416 9725 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11171 9725 603 41 0 11130 0
vsize: 44684
[startup+350.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29236
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10089 0 0 0 34975 26 0 0 25 0 1 0 481667367 45891584 9760 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11204 9760 603 41 0 11163 0
vsize: 44816
[startup+360.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10130 0 0 0 35975 26 0 0 25 0 1 0 481667367 46153728 9801 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11268 9801 603 41 0 11227 0
vsize: 45072
[startup+370.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10215 0 0 0 36975 27 0 0 25 0 1 0 481667367 46424064 9886 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9886 603 41 0 11293 0
vsize: 45336
[startup+380.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10215 0 0 0 37975 27 0 0 25 0 1 0 481667367 46424064 9886 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9886 603 41 0 11293 0
vsize: 45336
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10215 0 0 0 38975 27 0 0 25 0 1 0 481667367 46424064 9886 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9886 603 41 0 11293 0
vsize: 45336
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10215 0 0 0 39975 27 0 0 25 0 1 0 481667367 46424064 9886 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9886 603 41 0 11293 0
vsize: 45336
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10219 0 0 0 40975 27 0 0 25 0 1 0 481667367 46424064 9890 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9890 603 41 0 11293 0
vsize: 45336
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10222 0 0 0 41976 27 0 0 25 0 1 0 481667367 46424064 9893 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9893 603 41 0 11293 0
vsize: 45336
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10223 0 0 0 42976 27 0 0 25 0 1 0 481667367 46424064 9894 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9894 603 41 0 11293 0
vsize: 45336
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10223 0 0 0 43976 27 0 0 25 0 1 0 481667367 46424064 9894 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9894 603 41 0 11293 0
vsize: 45336
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10223 0 0 0 44976 27 0 0 25 0 1 0 481667367 46424064 9894 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 9894 603 41 0 11293 0
vsize: 45336
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 0 10314 0 0 0 45976 27 0 0 25 0 1 0 481667367 46424064 9985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11334 9985 603 41 0 11293 0
vsize: 45336
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 4 10320 0 0 0 46974 29 0 0 25 0 1 0 481667367 0 0 4294967295 0 0 0 0 0 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29238
Raw data (stat): 29234 (minisat+) R 29233 20838 20837 0 -1 4 10320 0 0 0 46974 29 0 0 25 0 1 0 481667367 0 0 4294967295 0 0 0 0 0 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0

Child status: 30
Real time (s): 470.015
CPU time (s): 470.047
CPU user time (s): 469.746
CPU system time (s): 0.300954
CPU usage (%): 100.007
Max. virtual memory (Kb): 45336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####