Suppose we have:

- two sets of facts,
`{fact1, fact2}`

and`{fact3, fact4}`

, among others - two tests
`s`

and`t`

, with the following rules, plus possibly others which don't involve these facts or test results:

s-result1 IF f`act`

1 s-result1 IF f`act`

3 ... t-result1 IF f`act`

1 t-result1 IF f`act`

4 ...

Now assume that the student gets `s-result1`

and
`t-result1`

, and the question is "Is `fact2`

consistent with those results?"

Since `fact2`

doesn't predict any results, it can't be
ruled out directly by any result that does or doesn't occur. And yet
`fact2`

is, in fact, provably inconsistent with the above
results. Why? Because

- If
`s-result1`

and`t-result1`

are both true, then`fact1 OR fact3`

and`fact1 OR fact4`

are both true. `fact3`

and`fact4`

can't both be true, therefore one has to be false.- Making either one false means
`fact1`

has to be true. `fact1`

and`fact2`

can't both be true, so`fact2`

has to be false.

Hence, even if the rules were constrained to single causes, which they weren't, you would still need something equivalent to a propositional theorem prover.