A theorem, T1 → T0, which easily implies the query was found in the database.
Theorem
| Hypothesis: | T1 and T4 and not T0 |
| Conclusion: | T3.5 |
Note: This selection of hypothesis and conclusion is only one way to interpret this theorem. The theorem could be written as many different logically equivalent implications.