superfluous axioms

[arademaker]

/*
(forall (?ROW0 ?ROW1 ?ROW2)
 (=> (and (instance ?ROW1 Class) (instance ?ROW0 Class) (instance ?ROW2 Class))
  (=>
   (and (subrelation exhaustiveDecomposition exhaustiveDecomposition)
    (and (instance exhaustiveDecomposition Predicate)
     (and (instance exhaustiveDecomposition Predicate)
      (exhaustiveDecomposition3 ?ROW0 ?ROW1 ?ROW2))))
   (exhaustiveDecomposition3 ?ROW0 ?ROW1 ?ROW2))))
*/
fof(a31410,axiom,! [ROW0,ROW1,ROW2] : (((s_instance(ROW1, s_Class) & s_instance(ROW0, s_Class) & s_instance(ROW2, s_Class)) => ((s_subrelation(s_exhaustiveDecomposition_m, s_exhaustiveDecomposition_m) & (s_instance(s_exhaustiveDecomposition_m, s_Predicate) & (s_instance(s_exhaustiveDecomposition_m, s_Predicate) & s_exhaustiveDecomposition3(ROW0, ROW1, ROW2)))) => s_exhaustiveDecomposition3(ROW0, ROW1, ROW2))))).

[arademaker]

Investigating this error, I found a new problem. The function that looks for predicate variables is considering that the two axioms below contain predicate variables:

(=>
 (and
  (instance ?Bond CallableBond)
  (currentAccountBalance (AccountFn ?Bond) ?Date ?Amount)
  (callDate ?Bond ?Date))
 (amountDue (AccountFn ?Bond) ?Amount ?Date))

(=>
 (albumRelease ?A ?T)
 (and
  (exists (?R1 ?DS1)
   (releaseForSale (AlbumCopiesFn ?A ?DS1) ?R1 ?T))
  (not
   (exists (?B ?R2 A?DS2)
    (and
     (before ?B ?T)
     (releaseForSale
      (AlbumCopiesFn ?A ?DS2) ?R2 ?B))))))

The problem is in the way the fuction map-fold and find-vars operate. They should maintain a context during the parsing of the axiom.

[arademaker]

Once this is solved, we must take care to not substitute different predicate variables in the same axiom by the same predicate symbol.