- for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) {
- Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o,d);
- if (nonNull(ev))
- return ev;
- }
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes) {
+ int i;
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fputs("scEntail(scFind): ", stdout);
+ printContext(stdout,copyPreds(ps));
+ fputs(" ||- ", stdout);
+ printPred(stdout, copyPred(pi, o));
+ fputc('\n', stdout);
+ }
+#endif
+ improve1(0,ps,pi,o);
+ ev = scEntail(ps,pi,o,d);
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes && nonNull(ev)) {
+ int i;
+ for (i = 0; i < d; i++)
+ fputc(' ', stdout);
+ fputs("scSat.\n", stdout);
+ }
+#endif
+ return ev;