Over the past 25 years, researchers have written numerous deduction systems based on resolution and paramodulation. Of these systems, a very few have been capable of generating and maintaining a formula database "containing more than just a few thousand clauses. These few systems were used to explore mechanisms for rapidly extracting limited subsets of relevant" clauses. We have written this tutorial to reflect some of the best ideas that have emerged and to cast them in a form that makes them easily accessible to students wishing to write their own high-performance systems.

Fluid-elastic instability of loosely supported tubes, vibrating in a tube-support-plate (TSP) inactive mode, is suspected to be one of the main causes of tube failure in some operating steam generators and heat exchangers. This report presents a mathematical model for fluid-elastic instability of loosely supported tubes exposed to non-uniform cross-flow. The model incorporates all motion-dependent fluid forces based on the unsteady flow theory. In the unstable region associated with a TSP-inactive mode, tube motion can be described by two linear models: TSP-inactive mode when tubes do not strike the TSP, and TSP-active mode when tubes do strike the TSP. A bilinear model (consisting of these linear models) presented in this report simulates the characteristics of fluid-elastic instability of loosely supported tubes in stable and unstable regions associated with TSP-inactive modes. Analytical results obtained with the model are compared with published experimental data; they agree reasonably well. The prediction procedure presented for fluid-elastic instability response of loosely supported tubes is applicable to the stable and unstable regions of the TSP-inactive mode.