# Why does Vampire give a refutation for axiom "lecturer(fr)" and conjecture "lecturer(fr)"?

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Why does Vampire give a refutation for axiom “lecturer(fr)” and conjecture “lecturer(fr)”?
Using http://www.tptp.org/cgi-bin/SystemOnTPTP and Vampire there, I am trying out the following:

```fof(4, axiom, lecturer(fr)). fof(query, conjecture, lecturer(fr)).```

Why does that find a refutation?

```% Refutation found. Thanks to Tanya! % SZS status Theorem for SOT_z1GY % SZS output start Proof for SOT_z1GY fof(f7,plain,( \$false), inference(subsumption_resolution,[],[f6,f5])). fof(f5,plain,( ~lecturer(fr)), inference(cnf_transformation,[],[f4])). fof(f4,plain,( ~lecturer(fr)), inference(flattening,[],[f3])). fof(f3,negated_conjecture,( ~lecturer(fr)), inference(negated_conjecture,[],[f2])). fof(f2,conjecture,( lecturer(fr)), file('/tmp/RjiEQ76n1Q/SOT_z1GYCV',query)). fof(f6,plain,( lecturer(fr)), inference(cnf_transformation,[],[f1])). fof(f1,axiom,( lecturer(fr)), file('/tmp/RjiEQ76n1Q/SOT_z1GYCV',4)). % SZS output end Proof for SOT_z1GY % ------------------------------ % Version: Vampire 4.5.0 (commit 2ee491ce on 2020-06-19 13:55:12 +0100) % Termination reason: Refutation ```

On the other hand, Vampire says the following is satisfiable:

```fof(4, axiom, lecturer(fr)). fof(query, conjecture, ~lecturer(fr)).```

Vampire negates the conjecture. That’s how classical FOL theorem provers tend to see the world.