# What does "EquationalLogicFindCounterexample[]" do?

I found the undocumented EquationalLogicFindCounterexample[] by browsing the lists of available symbols, but I have no clue about its purpose.

The name is intriguing!

So far I found the following:

• Accepts 2 or 3 arguments
• Returns an Integer (1, 10, 15, 31, 100 ...)
• For the first two arguments it seems to need equalities and boolean expressions (I didn't try quantifiers yet). Like in

EquationalLogicFindCounterexample[r == r + 1  && r == 2, b == 1]

• For the third argument, almost anything is allowed
• The numeric result seems to be connected to some feature of the equation system, but not sure to which one.

For example:

EquationalLogicFindCounterexample[r == a + 1  , a == 1]
(*
-> 31
*)

EquationalLogicFindCounterexample[r == a + 1  , r == a]
(*
-> 100
*)


Any suggestions or ideas about how to use this?

Edit

Some additional info, mostly provided by @Rojo:

Names["EquationalLogic*"] // Column
(*
"EquationalLogicFindCounterexample"
"EquationalLogicFindProof"
"EquationalLogicProve"
"EquationalLogic$MaxCounterexampleSearchSize" "EquationalLogic$ProverOptions"
*)


All interesting names!

Now, look at this:

EquationalLogicFindProof[y == x, y == 2 && x == 2]
(*
{ProofObject[
InitialLemma[1, 2 == x],
InitialLemma[2, 2 == y],
InitialHypothesis[3, y == x],
OrientRule[4, 2 -> x, Reason[1, Identity, 1]],
ApplyLemma[5, 2 -> x, 2 == y, 0, 1, DeducedLemma[5, x == y, SupportingReason[2, x, x, 4, 0]]],
OrientRule[6, x -> y, Reason[5, Identity, 2]],
ApplyLemma[8, y -> x, y == x, 0, 1, SufficesToShow[8, True, SupportingReason[3, x, x, 6, 1]]],
FinalGoal[9, True, EndReason]
], True}


EquationalLogicFindProof[2 y == 2 x, y == 2 && x == 2]
(*
{ProofObject[], False}
*)


If you run

Trace[EquationalLogicFindProof[x == 0, x == 0], TraceInternal -> True]


among a lot of non human gibberish, you will find a lot of references to