The Taelja Effect

The Problem

• Prove ((((true ⊕ false) ⊕ false) ⊕ true) ⊕ false) = false
• In the TPTP MSC005-1.p

The Refutation

• By E - Proof DAG
• In LLM English The prover starts by assuming that ((((true ⊕ false) ⊕ false) ⊕ true) ⊕ false) has no truth value. It then works backwards through the nested expression, establishing successively that (((true ⊕ false) ⊕ false) ⊕ true) != false, then ((true ⊕ false) ⊕ false) != true, and finally (true ⊕ false) != true. However, the axioms specify that (true ⊕ false) = true. This contradiction refutes the original assumption, proving that ((((true ⊕ false) ⊕ false) ⊕ true) ⊕ false) = false.

The Proof

• After Taelja - Proof DAG

  cnf(false_xor_false,axiom,
      ( ~ value(X2,falsity)
      | ~ value(X1,falsity)
      | value(xor(X1,X2),falsity) ),
      file('/export/starexec/sandbox2/benchmark/theBenchmark.p',false_xor_false) ).
  
  cnf(false_is_false,axiom,
      value(falsity,falsity),
      file('/export/starexec/sandbox2/benchmark/theBenchmark.p',false_is_false) ).
  
  cnf(true_xor_true,axiom,
      ( ~ value(X2,truth)
      | ~ value(X1,truth)
      | value(xor(X1,X2),falsity) ),
      file('/export/starexec/sandbox2/benchmark/theBenchmark.p',true_xor_true) ).
  
  cnf(true_is_true,axiom,
      value(truth,truth),
      file('/export/starexec/sandbox2/benchmark/theBenchmark.p',true_is_true) ).
  
  cnf(true_xor_false,axiom,
      ( ~ value(X2,falsity)
      | ~ value(X1,truth)
      | value(xor(X1,X2),truth) ),
      file('/export/starexec/sandbox2/benchmark/theBenchmark.p',true_xor_false) ).
  
  fof(lemma_6,lemma,
      value(xor(truth,falsity),truth),
      inference(mp,[status(thm)],[true_xor_false,false_is_false,true_is_true]) ).
  
  fof(lemma_7,lemma,
      value(xor(xor(truth,falsity),falsity),truth),
      inference(mp,[status(thm)],[true_xor_false,false_is_false,lemma_6]) ).
  
  fof(lemma_8,lemma,
      value(xor(xor(xor(truth,falsity),falsity),truth),falsity),
      inference(mp,[status(thm)],[true_xor_true,true_is_true,lemma_7]) ).
  
  fof(goal_1,theorem,
      value(xor(xor(xor(xor(truth,falsity),falsity),truth),falsity),falsity),
      inference(mp,[status(thm)],[false_xor_false,false_is_false,lemma_8]) ).
  

• In LLM English The proof first establishes that (true ⊕ false) = true, using the XOR axiom. It then establishes that ((true ⊕ false) ⊕ false) = true, again applying the XOR axiom. Next, it establishes that (((true ⊕ false) ⊕ false) ⊕ true) = false, since (true ⊕ true) = false. Finally, applying the false ⊕ false axiom proves that ((((true ⊕ false) ⊕ false) ⊕ true) ⊕ false) = false.

The Magic