+#if EXPLAIN_INSTANCE_RESOLUTION
+ else {
+ if (showInstRes) {
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fputs("No instance found for ", stdout);
+ printPred(stdout, copyPred(pi, o));
+ fputc('\n', stdout);
+ }
+ }
+#endif
+ return NIL;
+#if TREX
+ }
+#endif
+}
+
+#if MULTI_INST
+static Cell local inEntails(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
+List ps; /* using a top-level instance */
+Cell pi; /* entailment */
+Int o;
+Int d; {
+ int i;
+ int k = 0;
+ Cell ins; /* Class predicates */
+ Inst in, in_;
+ Cell e_;
+
+ if (d++ >= cutoff)
+ cutoffExceeded(pi,o,ps);
+
+#if TREX
+ if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
+ Cell e = fun(pi);
+ Cell l;
+ l = lacksNorm(arg(pi),o,e);
+ if (isNull(l) || isInt(l))
+ return l;
+ else {
+ List qs = ps;
+ for (; nonNull(qs); qs=tl(qs)) {
+ Cell qi = fst3(hd(qs));
+ if (isAp(qi) && fun(qi)==e) {
+ Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
+ if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
+ Int f = intOf(snd(l)) - intOf(snd(lq));
+ return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
+ mkInt(f),
+ thd3(hd(qs)));
+ }
+ }
+ }
+ return NIL;
+ }
+ }
+ else {
+#endif
+
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes) {
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fputs("inEntails: ", stdout);
+ printContext(stdout,copyPreds(ps));
+ fputs(" ||- ", stdout);
+ printPred(stdout, copyPred(pi, o));
+ fputc('\n', stdout);
+ }
+#endif
+
+ ins = findInstsFor(pi,o);
+ for (; nonNull(ins); ins=tl(ins)) {
+ in = snd(hd(ins));
+ if (nonNull(in)) {
+ Int beta = fst(hd(ins));
+ Cell e = inst(in).builder;
+ Cell es = inst(in).specifics;
+
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes) {
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fputs("try ", stdout);
+ printContext(stdout, es);
+ fputs(" => ", stdout);
+ printPred(stdout, inst(in).head);
+ fputc('\n', stdout);
+ }
+#endif
+
+ for (; nonNull(es); es=tl(es)) {
+ Cell ev = entail(ps,hd(es),beta,d);
+ if (nonNull(ev))
+ e = ap(e,ev);
+ else {
+ e = NIL;
+ break;
+ }
+ }
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes)
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+#endif
+ if (nonNull(e)) {
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes)
+ fprintf(stdout, "Sat\n");
+#endif
+ if (k > 0) {
+ if (instCompare (in_, in)) {
+ ERRMSG(0) "Multiple satisfiable instances for "
+ ETHEN
+ ERRPRED(copyPred(pi, o));
+ ERRTEXT "\nin_ " ETHEN ERRPRED(inst(in_).head);
+ ERRTEXT "\nin " ETHEN ERRPRED(inst(in).head);
+ ERRTEXT "\n"
+ EEND;
+ }
+ }
+ if (k++ == 0) {
+ e_ = e;
+ in_ = in;
+ }
+ continue;
+ } else {
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes)
+ fprintf(stdout, "not Sat\n");
+#endif
+ continue;
+ }
+ }
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes) {
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fprintf(stdout, "not Sat.\n");
+ }
+#endif
+ }
+ if (k > 0)
+ return e_;
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes) {
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fprintf(stdout, "all not Sat.\n");
+ }
+#endif