The quantity and quality of the trace file depends on the selected verbosity level of zdatrinf and ranges from showing just query results without the query or the final full stop at verbosity level -2, to a complete trace including all used rules and (for debugging purposes) all detected atoms and nodes at verbosity level 3.
With tracing enabled (verbosity level 1 or higher) several kinds of information about inferences are provided, including the inference rule number and:
=i,j,k> LOCAL localnode:< matchedpath || unmatched path > == rhs
GLOBAL globalnode:< globalpath >
Small letters indicate variables:
To illustrate a typical trace presume the following (silly) theory:
A: <> == ample <a> == <<b>> <b> == c <c> == <d> "A:<>" <d> == ex.A typical output for verbosity level 1 is shown in the example below. The first line is the manual query input, the last two lines are the statistics and the result.
#1=> A:<a>
=0,0,0> LOCAL A:< a > == < < b > >
GLOBAL A:< a >
=1,1,0> LOCAL A:< b > == c
GLOBAL A:< a >
=1,0,0> LOCAL A:< c > == < d > "A: < > "
GLOBAL A:< a >
=2,0,0> LOCAL A:< d > == ex
GLOBAL A:< a >
=2,0,1> LOCAL A:< > == ample
GLOBAL A:< >
[Query 1 (7 Inferences)] A:< a >
= ex ample .