BETH-TREE METHODS IN AUTOMATIC THEOREM-PROVING

In the'condition omitted' column: denotes that the full complement of heuristic devices was in use denotes that the coefficient of the feature L was set to zero denotes that the coefficient of the feature B was set to zero de,notes that the coefficient of the feature E was set to zero denotes that the coefficient of the feature T was set to zero PD denotes that all neighbours of a node were produced at one development M denotes that the example group was not in use 44 POPPLESTONE F denotes that the equality was proved in reverse, i.e., that the RHS was converted into the LHS. Note that the LHS is longer than the RHS in every problem where the lengths are different. In the'result' column: S denotes that the problem was solved F denotes that the problem was unsolved after 100 distinct nodes had been produced - FF denotes that the problem was unsolved after 100 distinct nodes had been produced but that the problem was solved after restarting one or more times from the most promising node produced so far (see Doran's paper in this volume). FL denotes that the problem was unsolved because a term too large to hold in the array assigned to hold it was produced. The nodes listed' column gives the total number of distinct nodes produced.