Open wo opened 7 months ago
I think this happens because the modelfinder uses numerals as terms, and gets confused with the numeric constants in the input formulas.
There's another problem: if I disable the modelfinder, ∀xc(x,1)=1,∀x(x=1↔¬x=0),∀xc(0,x)=1|=c(a,c(b,b))=1
is proved almost instantaneously, but with letters instead of the numerals the prover is painfully slow: ∀xc(x,q)=q,∀x(x=q↔¬x=z),∀xc(z,x)=q|=c(a,c(b,b))=q
The first relevant difference in the proof search is this:
# trying rrbs
checking if candidate terms [c,a,[c,b,b]] and 1 can be unified
can't add [c,a,[c,b,b]]=1 to constraint [{ }]
trying rrbs with [c,a,[c,b,b]] as si and 1 as ti
[add [c,a,[c,b,b]]>1 to { }?] function symbol of [c,a,[c,b,b]] is greater
[c,a,[c,b,b]]>1 is already entailed by [{ }]
trying [c,0,ξ1] as l and 1 as r
[add [c,0,ξ1]>1 to { }?] function symbol of [c,0,ξ1] is greater
[c,0,ξ1]>1 is already entailed by [{ }]
versus
# trying rrbs
checking if candidate terms [c,a,[c,b,b]] and q can be unified
can't add [c,a,[c,b,b]]=q to constraint [{ }]
trying rrbs with [c,a,[c,b,b]] as si and q as ti
[add [c,a,[c,b,b]]>q to { }?] function symbol in 2nd term is greater; one arg in 1st must be >= 1st term
[add a>q to { }?] function symbol in 2nd term is greater; one arg in 1st must be >= 1st term
[add [c,b,b]>q to { }?] function symbol in 2nd term is greater; one arg in 1st must be >= 1st term
[add b>q to { }?] function symbol in 2nd term is greater; one arg in 1st must be >= 1st term
[add b>q to { }?] function symbol in 2nd term is greater; one arg in 1st must be >= 1st term
[add [c,b,b]>q to { }?] result: []
[add [c,a,[c,b,b]]>q to { }?] result: []
can't add [c,a,[c,b,b]]>q to constraint [{ }]
trying rrbs with q as si and [c,a,[c,b,b]] as ti
If I change around the letters, it goes back to almost instantaneous: ∀xf(x,c)=c,∀x(x=c↔¬x=d),∀xf(d,x)=c|=f(a,f(b,b))=c
So there's no obvious bug in the prover, but possible room for improvement.
∀xc(x,1)=1,∀x(x=1↔¬x=0),∀xc(0,x)=1|= c(a,c(b,b))=1
is valid, but the modelfinder presents a countermodel.