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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-1.opb
MD5SUM	84d0b0ba659c599a6c66454cd956a06b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04684
Number of variables	450
Total number of constraints	17827
Number of constraints which are clauses	17827
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6338

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 04:33:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4826 boxname=wulflinc28 idbench=314 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  84d0b0ba659c599a6c66454cd956a06b  /oldhome/oroussel/tmp/wulflinc28/normalized-frb30-15-1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc28/normalized-frb30-15-1.opb /oldhome/oroussel/tmp/wulflinc28/normalized-frb30-15-1.opb
IDLAUNCH: 4826
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        882916 kB
Buffers:         35984 kB
Cached:          78660 kB
SwapCached:          4 kB
Active:          56396 kB
Inactive:        62036 kB
HighTotal:      131008 kB
HighFree:        47796 kB
LowTotal:       903652 kB
LowFree:        835120 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27752 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:41:04 (client local time) WITH STATUS 30 IN 475.996 SECONDS
stats: 4826 0 475.996 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17827 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17827    35654 |    5942       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   52015   115763 |   17338       0        0     nan |  0.000 % |
c |       100 |   50756   112891 |   19071      66      323     4.9 |  3.252 % |
c |       250 |   49418   109825 |   20978     164     1389     8.5 |  6.744 % |
c |       475 |   46882   104034 |   23076     309     2327     7.5 | 13.240 % |
c ==============================================================================
c [1mFound solution: -23[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 |       580 |   46145   102440 |   15381     390     3272     8.4 | 13.240 % |
c |       681 |   45679   101359 |   16919     475     4222     8.9 | 17.299 % |
c |       831 |   44447    98523 |   18611     601     4890     8.1 | 20.576 % |
c |      1056 |   42167    93247 |   20472     764     6321     8.3 | 26.639 % |
c |      1393 |   40240    88775 |   22519    1055     9446     9.0 | 31.964 % |
c |      1899 |   36999    81217 |   24771    1420    13601     9.6 | 40.797 % |
c |      2658 |   33556    73180 |   27248    1973    19930    10.1 | 51.634 % |
c |      3797 |   28986    62491 |   29973    2559    30526    11.9 | 63.480 % |
c ==============================================================================
c [1mFound solution: -24[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 |      4392 |   27869    59817 |    9289    3006    42271    14.1 | 63.480 % |
c |      4492 |   27663    59329 |   10217    3061    43504    14.2 | 67.415 % |
c |      4642 |   27623    59235 |   11239    3200    52349    16.4 | 67.533 % |
c |      4867 |   27449    58826 |   12363    3396    55017    16.2 | 68.050 % |
c ==============================================================================
c [1mFound solution: -25[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 |      5186 |   27094    58005 |    9031    3631    61705    17.0 | 68.050 % |
c |      5286 |   27014    57820 |    9934    3712    64082    17.3 | 69.491 % |
c |      5438 |   26866    57476 |   10927    3849    69097    18.0 | 69.913 % |
c |      5663 |   26348    56257 |   12020    3972    75061    18.9 | 71.467 % |
c |      6001 |   25560    54391 |   13222    4076    81053    19.9 | 73.875 % |
c |      6507 |   25560    54391 |   14544    4582   107988    23.6 | 73.874 % |
c |      7266 |   25069    53236 |   15998    5125   122692    23.9 | 75.336 % |
c ==============================================================================
c [1mFound solution: -26[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 |      8397 |   24829    52641 |    8276    6071   146319    24.1 | 75.336 % |
c |      8497 |   24668    52257 |    9103    6097   146945    24.1 | 76.522 % |
c |      8647 |   24662    52243 |   10013    6246   150684    24.1 | 76.539 % |
c |      8872 |   24628    52163 |   11015    6437   161710    25.1 | 76.919 % |
c |      9210 |   24240    51252 |   12116    6544   164403    25.1 | 77.789 % |
c |      9717 |   24240    51252 |   13328    7051   196286    27.8 | 77.789 % |
c |     10476 |   24082    50884 |   14661    7637   224438    29.4 | 78.237 % |
c |     11616 |   24082    50884 |   16127    8777   273581    31.2 | 78.237 % |
c |     13324 |   23793    50194 |   17740   10146   376347    37.1 | 79.140 % |
c ==============================================================================
c [1mFound solution: -27[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 |     13939 |   23841    50318 |    7947   10757   403133    37.5 | 79.140 % |
c |     14039 |   23841    50318 |    8741   10857   406504    37.4 | 79.184 % |
c |     14189 |   23841    50318 |    9615   11007   419075    38.1 | 79.183 % |
c |     14414 |   23763    50135 |   10577   11176   428520    38.3 | 79.418 % |
c |     14751 |   23763    50135 |   11635   11513   445546    38.7 | 79.418 % |
c |     15257 |   23690    49966 |   12798   11967   473668    39.6 | 79.619 % |
c |     16016 |   23690    49966 |   14078   12726   520632    40.9 | 79.620 % |
c |     17155 |   23603    49763 |   15486   13671   584407    42.7 | 79.871 % |
c |     18864 |   23510    49541 |   17035   15282   689604    45.1 | 80.173 % |
c |     21426 |   23504    49527 |   18738   17843   858550    48.1 | 80.190 % |
c |     25270 |   23504    49527 |   20612   21687  1123981    51.8 | 80.189 % |
c |     31038 |   23472    49450 |   22673   27379  1506411    55.0 | 80.298 % |
c ==============================================================================
c [1mFound solution: -28[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 |     37208 |   23449    49384 |    7816   33457  1903821    56.9 | 80.298 % |
c |     37308 |   23449    49384 |    8597   14779   785176    53.1 | 80.361 % |
c |     37459 |   23449    49384 |    9457   14930   790239    52.9 | 80.360 % |
c |     37684 |   23400    49270 |   10403   15153   801280    52.9 | 80.495 % |
c |     38021 |   23400    49270 |   11443   15490   824145    53.2 | 80.495 % |
c |     38527 |   23400    49270 |   12587   15996   854130    53.4 | 80.495 % |
c |     39287 |   23115    48604 |   13846   16662   895341    53.7 | 81.325 % |
c |     40426 |   23083    48529 |   15231   17762   980262    55.2 | 81.417 % |
c |     42134 |   23083    48529 |   16754   19470  1068579    54.9 | 81.417 % |
c |     44697 |   23083    48529 |   18429   22033  1209148    54.9 | 81.417 % |
c |     48542 |   23083    48529 |   20272   25878  1342675    51.9 | 81.417 % |
c |     54309 |   23083    48529 |   22299   15643   479794    30.7 | 81.417 % |
c |     62960 |   23083    48529 |   24529   24294   756884    31.2 | 81.417 % |
c ==============================================================================
c [1mFound solution: -29[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 |     63850 |   23113    48602 |    7704   25184   790906    31.4 | 81.417 % |
c |     63952 |   23113    48602 |    8474   12694   333475    26.3 | 81.375 % |
c |     64102 |   23113    48602 |    9321   12844   338586    26.4 | 81.375 % |
c |     64327 |   23113    48602 |   10254   13069   345888    26.5 | 81.375 % |
c |     64665 |   23113    48602 |   11279   13407   355537    26.5 | 81.375 % |
c |     65171 |   23113    48602 |   12407   13913   372611    26.8 | 81.375 % |
c |     65931 |   23113    48602 |   13648   14673   399449    27.2 | 81.375 % |
c |     67070 |   23113    48602 |   15012   15812   427232    27.0 | 81.375 % |
c |     68778 |   23113    48602 |   16514   17520   468239    26.7 | 81.375 % |
c |     71340 |   23113    48602 |   18165   20082   528573    26.3 | 81.375 % |
c |     75185 |   23113    48602 |   19982   23927   631645    26.4 | 81.375 % |
c |     80951 |   23113    48602 |   21980   29693   846455    28.5 | 81.375 % |
c |     89600 |   23105    48583 |   24178   21869   753291    34.4 | 81.400 % |
c |    102574 |   22934    48186 |   26596   17238   419657    24.3 | 81.885 % |
c |    122036 |   22879    48056 |   29255   36674  1125370    30.7 | 82.061 % |
c |    151228 |   22848    47985 |   32181   19509   458614    23.5 | 82.144 % |
c |    195017 |   22543    47265 |   35399   37056  1107449    29.9 | 82.705 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7690     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    197690 |   29898    64400 |    9966   39729  1180129    29.7 | 82.705 % |
c |    197792 |   29898    64400 |   10962   18879   437896    23.2 | 70.562 % |
c |    197943 |   29898    64400 |   12058   19030   442630    23.3 | 70.562 % |
c |    198168 |   29898    64400 |   13264   19255   447928    23.3 | 70.562 % |
c |    198507 |   29898    64400 |   14591   19594   458078    23.4 | 70.562 % |
c |    199013 |   29898    64400 |   16050   20100   470090    23.4 | 70.562 % |
c |    199772 |   29898    64400 |   17655   20859   491075    23.5 | 70.562 % |
c |    200911 |   29762    64098 |   19420   21987   516495    23.5 | 70.847 % |
c |    202620 |   29754    64079 |   21363   23695   561251    23.7 | 70.866 % |
c |    205183 |   29748    64065 |   23499   26256   628182    23.9 | 70.879 % |
c |    209028 |   29701    63959 |   25849   30100   730265    24.3 | 70.963 % |
c |    214796 |   29654    63853 |   28434   35867   915196    25.5 | 71.047 % |
c |    223445 |   29409    63261 |   31277   35123   913406    26.0 | 71.630 % |
c |    236419 |   29409    63261 |   34405   26096   640902    24.6 | 71.630 % |
c |    255880 |   29409    63261 |   37845   45557  1272596    27.9 | 71.630 % |
c |    285073 |   28366    61031 |   41630   36414  1063381    29.2 | 72.660 % |
c |    328862 |   26065    56131 |   45793   22077   508186    23.0 | 74.707 % |
c ==============================================================================
c [1mOptimal solution: -30[0m
s OPTIMUM FOUND
v -C450 -C449 -C448 C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 C336 -C335 -C334 -C333 -C332 -C331 -C330 C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 C211 -C210 -C209 -C208 -C207 C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 C122 -C121 C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 C78 -C77 -C76 -C75 C74 -C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 -C62 -C61 -C60 -C59 -C58 -C57 -C56 C55 -C54 -C53 -C52 -C51 -C50 -C49 -C48 -C47 -C46 -C45 -C44 -C43 -C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 C34 -C33 -C32 -C31 -C30 -C29 -C28 -C27 -C26 -C25 -C24 -C23 -C22 -C21 -C20 C19 -C18 -C17 -C16 -C15 -C14 -C13 -C12 -C11 -C10 -C9 -C8 -C7 -C6 C5 -C4 -C3 -C2 -C1
c _______________________________________________________________________________
c 
c restarts              : 92
c conflicts             : 335178         (704 /sec)
c decisions             : 407413         (856 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 475.78 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 21494
Raw data (stat): 21494 (runsolver) R 21493 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481745041 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 1641 0 0 0 994 4 0 0 25 0 1 0 481745041 8663040 1619 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2115 1619 603 41 0 2074 0
vsize: 8460
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 2232 0 0 0 1992 6 0 0 25 0 1 0 481745041 11071488 2210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2703 2210 603 41 0 2662 0
vsize: 10812
[startup+30.0012 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 2804 0 0 0 2990 8 0 0 25 0 1 0 481745041 13434880 2782 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3280 2782 603 41 0 3239 0
vsize: 13120
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3335 0 0 0 3988 11 0 0 25 0 1 0 481745041 15581184 3313 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3804 3313 603 41 0 3763 0
vsize: 15216
[startup+50.003 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3743 0 0 0 4987 12 0 0 25 0 1 0 481745041 17395712 3721 4294967295 134512640 134672761 3221224560 3221223748 1075346947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3721 603 41 0 4206 0
vsize: 16988
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3743 0 0 0 5986 13 0 0 25 0 1 0 481745041 17395712 3721 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3721 603 41 0 4206 0
vsize: 16988
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3743 0 0 0 6986 13 0 0 25 0 1 0 481745041 17395712 3721 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3721 603 41 0 4206 0
vsize: 16988
[startup+80.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3743 0 0 0 7985 14 0 0 25 0 1 0 481745041 17395712 3721 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3721 603 41 0 4206 0
vsize: 16988
[startup+90.0043 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3744 0 0 0 8985 14 0 0 25 0 1 0 481745041 17395712 3722 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3722 603 41 0 4206 0
vsize: 16988
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3744 0 0 0 9985 14 0 0 25 0 1 0 481745041 17395712 3722 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3722 603 41 0 4206 0
vsize: 16988
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3745 0 0 0 10985 15 0 0 25 0 1 0 481745041 17395712 3723 4294967295 134512640 134672761 3221224560 3221223792 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3723 603 41 0 4206 0
vsize: 16988
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3745 0 0 0 11985 15 0 0 25 0 1 0 481745041 17395712 3723 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3723 603 41 0 4206 0
vsize: 16988
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3745 0 0 0 12985 15 0 0 25 0 1 0 481745041 17395712 3723 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3723 603 41 0 4206 0
vsize: 16988
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3746 0 0 0 13984 16 0 0 25 0 1 0 481745041 17395712 3724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3724 603 41 0 4206 0
vsize: 16988
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3746 0 0 0 14983 17 0 0 25 0 1 0 481745041 17395712 3724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3724 603 41 0 4206 0
vsize: 16988
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3748 0 0 0 15983 17 0 0 25 0 1 0 481745041 17395712 3726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3726 603 41 0 4206 0
vsize: 16988
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3752 0 0 0 16983 17 0 0 25 0 1 0 481745041 17395712 3730 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4247 3730 603 41 0 4206 0
vsize: 16988
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3758 0 0 0 17983 18 0 0 25 0 1 0 481745041 17395712 3736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4247 3736 603 41 0 4206 0
vsize: 16988
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3770 0 0 0 18983 18 0 0 25 0 1 0 481745041 17543168 3748 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3748 603 41 0 4242 0
vsize: 17132
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3770 0 0 0 19983 18 0 0 25 0 1 0 481745041 17543168 3748 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3748 603 41 0 4242 0
vsize: 17132
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3775 0 0 0 20983 18 0 0 25 0 1 0 481745041 17543168 3753 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3753 603 41 0 4242 0
vsize: 17132
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3784 0 0 0 21983 18 0 0 25 0 1 0 481745041 17543168 3762 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3762 603 41 0 4242 0
vsize: 17132
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3787 0 0 0 22984 18 0 0 25 0 1 0 481745041 17543168 3765 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3765 603 41 0 4242 0
vsize: 17132
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3787 0 0 0 23984 18 0 0 25 0 1 0 481745041 17543168 3765 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3765 603 41 0 4242 0
vsize: 17132
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3787 0 0 0 24984 18 0 0 25 0 1 0 481745041 17543168 3765 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3765 603 41 0 4242 0
vsize: 17132
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3920 0 0 0 25984 18 0 0 25 0 1 0 481745041 17883136 3898 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3898 603 41 0 4325 0
vsize: 17464
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3920 0 0 0 26984 18 0 0 25 0 1 0 481745041 17883136 3898 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3898 603 41 0 4325 0
vsize: 17464
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3920 0 0 0 27985 18 0 0 25 0 1 0 481745041 17883136 3898 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3898 603 41 0 4325 0
vsize: 17464
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3920 0 0 0 28985 18 0 0 25 0 1 0 481745041 17883136 3898 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3898 603 41 0 4325 0
vsize: 17464
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3920 0 0 0 29985 18 0 0 25 0 1 0 481745041 17883136 3898 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3898 603 41 0 4325 0
vsize: 17464
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3921 0 0 0 30985 18 0 0 25 0 1 0 481745041 17883136 3899 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3899 603 41 0 4325 0
vsize: 17464
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3921 0 0 0 31985 18 0 0 25 0 1 0 481745041 17883136 3899 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3899 603 41 0 4325 0
vsize: 17464
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3921 0 0 0 32986 18 0 0 25 0 1 0 481745041 17883136 3899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3899 603 41 0 4325 0
vsize: 17464
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3921 0 0 0 33986 18 0 0 25 0 1 0 481745041 17883136 3899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3899 603 41 0 4325 0
vsize: 17464
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3925 0 0 0 34986 18 0 0 25 0 1 0 481745041 17883136 3903 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3903 603 41 0 4325 0
vsize: 17464
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3936 0 0 0 35986 18 0 0 25 0 1 0 481745041 18046976 3914 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3914 603 41 0 4365 0
vsize: 17624
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3936 0 0 0 36986 18 0 0 25 0 1 0 481745041 18046976 3914 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3914 603 41 0 4365 0
vsize: 17624
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3936 0 0 0 37986 18 0 0 25 0 1 0 481745041 18046976 3914 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3914 603 41 0 4365 0
vsize: 17624
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3936 0 0 0 38987 18 0 0 25 0 1 0 481745041 18046976 3914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3914 603 41 0 4365 0
vsize: 17624
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3936 0 0 0 39987 18 0 0 25 0 1 0 481745041 18046976 3914 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3914 603 41 0 4365 0
vsize: 17624
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 3936 0 0 0 40987 18 0 0 25 0 1 0 481745041 18046976 3914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3914 603 41 0 4365 0
vsize: 17624
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4047 0 0 0 41987 18 0 0 25 0 1 0 481745041 18452480 4025 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4025 603 41 0 4464 0
vsize: 18020
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4143 0 0 0 42987 19 0 0 25 0 1 0 481745041 18853888 4121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4121 603 41 0 4562 0
vsize: 18412
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4148 0 0 0 43987 19 0 0 25 0 1 0 481745041 18853888 4126 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4126 603 41 0 4562 0
vsize: 18412
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4148 0 0 0 44987 19 0 0 25 0 1 0 481745041 18853888 4126 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4126 603 41 0 4562 0
vsize: 18412
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4148 0 0 0 45987 19 0 0 25 0 1 0 481745041 18853888 4126 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4126 603 41 0 4562 0
vsize: 18412
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4148 0 0 0 46987 19 0 0 25 0 1 0 481745041 18853888 4126 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4126 603 41 0 4562 0
vsize: 18412
[startup+475.938 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 21494
Raw data (stat): 21494 (minisat+) R 21493 10614 10613 0 -1 0 4148 0 0 0 46987 19 0 0 25 0 1 0 481745041 18853888 4126 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4126 603 41 0 4562 0
vsize: 0

Child status: 30
Real time (s): 475.938
CPU time (s): 475.996
CPU user time (s): 475.795
CPU system time (s): 0.200969
CPU usage (%): 100.012
Max. virtual memory (Kb): 18412
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-30
#### END VERIFIER DATA ####