Motivating Example

The Venezuelan car manufacturer "Sucre" has been developing a futuristic electric car, called the Quipos. The Quipos has only three digital control circuits: the Energy Control Circuit (ECQ), the Wheel Control Circuit (WCQ), and the Human Haptics Detection (HHD) circuit. During development one of the circuits was repeatedly sending faulty signals to the WCQ, causing it to fail, with corresponding downstream impact on the car's self-steering and automatic braking features. The engineers needed to determine: Which circuit is sending the faulty signals to the WCQ?

The following facts are known about the signals being sent between the circuits:

Automated Theorem Proving was used to analyse this issue, and it turned out that ...

Another version