Which of the following statements are true?

In all answers are function symbols of arity 1, 2, and 3 respectively, is a constant symbol, and are variable symbols.

Given the following formula

(!x) & (x | y) & (x | !y | !z) & (!y | z).

Which formula do we get when eliminating variable x?

Important: 

• Use the operator symbols used above: write & for ∧, | for ∨, ! for ¬.
• Put clauses between ( and ) - as in the formula above. 
• Do not use any whitespaces. 

Given the formula

 (p ∨ q ∨ r) ∧ (¬t ∨ ¬s) ∧ (u ∨ s).

Which of the following clauses has the RUP property with respect to the given formula?

Which of the following statements hold?

Apply the Knuth-Bendix completion procedure to the reduction system

and the term order described below.

Assume a lexicographic ordering of the function symbols . The term order is defined by if

1. has fewer letters than and contains each variable at most as often as , or
2. if they have the same number of letters and variable occurrences, then if or and there is a such that for and .

Please submit a handwritten and readable solution in PDF format.

Consider the reduction system containing the following rules, where are function symbols of arity 1:

Which of the following terms constitute a critical pair for this reduction system?

Important: Since one can apply variable renamings in different ways, please consider the options below up to variable renaming. 

Which of the following terms can appear as output of Algorithm 3.21 if we apply the algorithm to the reduction system

and the term ?

Assuming that function symbols are sorted lexicographically (), consider the term order

Which of the following statements holds?

Given the following equational theories and equations.

Which of the following statements holds?