1:- set_prolog_flag(print_depth,1000). 2:- set_prolog_flag(variable_names,off). 3
4:- dynamic(count_inferences_pred/1). 5:- dynamic(trace_search_progress_pred/1). 6:- dynamic(compile_proof_printing/0). 7:- dynamic(ncalls/1). 8
22
23add_sound_unification((Head :- Body),(Head1 :- Body1)) :-
24 linearize(Head,Head1,[],_,true,Matches),
25 conjoin(Matches,Body,Body1).
26
27linearize(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut) :-
28 nonvar(TermIn) ->
29 functor(TermIn,F,N),
30 myfunctor(TermOut,F,N),
31 linearize_args(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut,1,N);
32 identical_member(TermIn,VarsIn) ->
33 VarsOut = VarsIn,
34 conjoin(MatchesIn,unify(TermIn,TermOut),MatchesOut);
35 36 TermOut = TermIn,
37 VarsOut = [TermIn|VarsIn],
38 MatchesOut = MatchesIn.
39
40linearize_args(TermIn,TermOut,VarsIn,VarsOut,MatchesIn,MatchesOut,I,N) :-
41 I > N ->
42 VarsOut = VarsIn,
43 MatchesOut = MatchesIn;
44 45 arg(I,TermIn,ArgI),
46 linearize(ArgI,NewArgI,VarsIn,Vars1,MatchesIn,Matches1),
47 arg(I,TermOut,NewArgI),
48 I1 is I + 1,
49 linearize_args(TermIn,TermOut,Vars1,VarsOut,Matches1,MatchesOut,I1,N).
50
54
55unify(X,Y) :-
56 var(X) ->
57 (var(Y) ->
58 X = Y;
59 60 functor(Y,_,N),
61 (N = 0 ->
62 true;
63 N = 1 ->
64 arg(1,Y,Y1), not_occurs_in(X,Y1);
65 66 not_occurs_in_args(X,Y,N)),
67 X = Y);
68 var(Y) ->
69 functor(X,_,N),
70 (N = 0 ->
71 true;
72 N = 1 ->
73 arg(1,X,X1), not_occurs_in(Y,X1);
74 75 not_occurs_in_args(Y,X,N)),
76 X = Y;
77 78 functor(X,F,N),
79 functor(Y,F,N),
80 (N = 0 ->
81 true;
82 N = 1 ->
83 arg(1,X,X1), arg(1,Y,Y1), unify(X1,Y1);
84 85 unify_args(X,Y,N)).
86
87unify_args(X,Y,N) :-
88 N = 2 ->
89 arg(2,X,X2), arg(2,Y,Y2), unify(X2,Y2),
90 arg(1,X,X1), arg(1,Y,Y1), unify(X1,Y1);
91 92 arg(N,X,Xn), arg(N,Y,Yn), unify(Xn,Yn),
93 N1 is N - 1, unify_args(X,Y,N1).
94
95not_occurs_in(Var,Term) :-
96 Var == Term ->
97 fail;
98 var(Term) ->
99 true;
100 101 functor(Term,_,N),
102 (N = 0 ->
103 true;
104 N = 1 ->
105 arg(1,Term,Arg1), not_occurs_in(Var,Arg1);
106 107 not_occurs_in_args(Var,Term,N)).
108
109not_occurs_in_args(Var,Term,N) :-
110 N = 2 ->
111 arg(2,Term,Arg2), not_occurs_in(Var,Arg2),
112 arg(1,Term,Arg1), not_occurs_in(Var,Arg1);
113 114 arg(N,Term,ArgN), not_occurs_in(Var,ArgN),
115 N1 is N - 1, not_occurs_in_args(Var,Term,N1).
116
150
151add_complete_search((Head :- Body),(Head1 :- Body1)) :-
152 Head =.. L,
153 append(L,[DepthIn,DepthOut],L1),
154 Head1 =.. L1,
155 (functor(Head,query,_) ->
156 add_complete_search_args(Body,DepthIn,DepthOut,Body1);
157 nonzero_search_cost(Body,Cost) ->
158 add_complete_search_args(Body,Depth1,DepthOut,Body2),
159 conjoin((DepthIn >= Cost , Depth1 is DepthIn - Cost),Body2,Body1);
160 161 add_complete_search_args(Body,DepthIn,DepthOut,Body1)).
162
163add_complete_search_args(Body,DepthIn,DepthOut,Body1) :-
164 Body = (A , B) ->
165 add_complete_search_args(A,DepthIn,Depth1,A1),
166 add_complete_search_args(B,Depth1,DepthOut,B1),
167 conjoin(A1,B1,Body1);
168 Body = (A ; B) ->
169 search_cost(A,CostA),
170 search_cost(B,CostB),
171 (CostA < CostB ->
172 add_complete_search_args(A,DepthIn,DepthOut,A1),
173 add_complete_search_args(B,Depth1,DepthOut,B2),
174 Cost is CostB - CostA,
175 conjoin((DepthIn >= Cost , Depth1 is DepthIn - Cost),B2,B1);
176 CostA > CostB ->
177 add_complete_search_args(A,Depth1,DepthOut,A2),
178 add_complete_search_args(B,DepthIn,DepthOut,B1),
179 Cost is CostA - CostB,
180 conjoin((DepthIn >= Cost , Depth1 is DepthIn - Cost),A2,A1);
181 182 add_complete_search_args(A,DepthIn,DepthOut,A1),
183 add_complete_search_args(B,DepthIn,DepthOut,B1)),
184 disjoin(A1,B1,Body1);
185 Body = search(Goal,Max,Min,Inc) ->
186 PrevInc is Min + 1,
187 add_complete_search_args(Goal,DepthIn1,DepthOut1,Goal1),
188 DepthIn = DepthOut,
189 Body1 = search(Goal1,Max,Min,Inc,PrevInc,DepthIn1,DepthOut1);
190 Body = search(Goal,Max,Min) ->
191 add_complete_search_args(search(Goal,Max,Min,1),DepthIn,DepthOut,Body1);
192 Body = search(Goal,Max) ->
193 add_complete_search_args(search(Goal,Max,0),DepthIn,DepthOut,Body1);
194 Body = search(Goal) ->
195 add_complete_search_args(search(Goal,1000000),DepthIn,DepthOut,Body1);
196 functor(Body,search_cost,_) ->
197 DepthIn = DepthOut,
198 Body1 = true;
199 builtin(Body) ->
200 DepthIn = DepthOut,
201 Body1 = Body;
202 203 Body =.. L,
204 append(L,[DepthIn,DepthOut],L1),
205 Body1 =.. L1.
206
207nonzero_search_cost(Body,Cost) :-
208 search_cost(Body,Cost),
209 Cost > 0.
210
220
221search_cost(Body,N) :-
222 Body = search_cost(M) ->
223 N = M;
224 Body = (A , B) ->
225 (A = search_cost(M) -> 226 N = M; 227 228 search_cost(A,N1),
229 search_cost(B,N2),
230 N is N1 + N2);
231 Body = (A ; B) ->
232 search_cost(A,N1),
233 search_cost(B,N2),
234 min(N1,N2,N);
235 builtin(Body) ->
236 N = 0;
237 functor(Body,_,2) -> 238 N = 0; 239 240 N = 1.
241
262
263search(Goal,Max,Min,Inc) :-
264 PrevInc is Min + 1,
265 add_complete_search_args(Goal,DepthIn,DepthOut,Goal1),
266 (compile_proof_printing ->
267 add_proof_recording_args(Goal1,_Proof,_ProofEnd,Goal2);
268 269 Goal2 = Goal1),
270 !,
271 search(Goal2,Max,Min,Inc,PrevInc,DepthIn,DepthOut).
272
273search(Goal,Max,Min) :-
274 search(Goal,Max,Min,1).
275
276search(Goal,Max) :-
277 search(Goal,Max,0).
278
279search(Goal) :-
280 search(Goal,1000000).
281
286
287search(_Goal,Max,Min,_Inc,_PrevInc,_DepthIn,_DepthOut) :-
288 Min > Max,
289 !,
290 fail.
291search(Goal,_Max,Min,_Inc,PrevInc,DepthIn,DepthOut) :-
292 trace_search_progress_pred(P1),
293 L1 =.. [P1,Min],
294 call(L1),
295 DepthIn = Min,
296 call(Goal),
297 DepthOut < PrevInc. 298search(Goal,Max,Min,Inc,_PrevInc,DepthIn,DepthOut) :-
299 Min1 is Min + Inc,
300 search(Goal,Max,Min1,Inc,Inc,DepthIn,DepthOut).
301
325
326add_ancestor((Head :- Body),(Head1 :- Body1)) :-
327 functor(Head,query,_) ->
328 Head1 = Head,
329 add_ancestor_args(Body,[[],[]],Body1);
330 331 Head =.. L,
332 append(L,[PosAncestors,NegAncestors],L1),
333 Head1 =.. L1,
334 add_ancestor_args(Body,[NewPosAncestors,NewNegAncestors],Body2),
335 (Body == Body2 ->
336 Body1 = Body2;
337 negative_literal(Head) ->
338 NewPosAncestors = PosAncestors,
339 conjoin((NewNegAncestors = [Head|NegAncestors]),Body2,Body1);
340 341 NewNegAncestors = NegAncestors,
342 conjoin((NewPosAncestors = [Head|PosAncestors]),Body2,Body1)).
343
344add_ancestor_args(Body,AncestorLists,Body1) :-
345 Body = (A , B) ->
346 add_ancestor_args(A,AncestorLists,A1),
347 add_ancestor_args(B,AncestorLists,B1),
348 conjoin(A1,B1,Body1);
349 Body = (A ; B) ->
350 add_ancestor_args(A,AncestorLists,A1),
351 add_ancestor_args(B,AncestorLists,B1),
352 disjoin(A1,B1,Body1);
353 Body =.. [search,Goal|L] ->
354 add_ancestor_args(Goal,AncestorLists,Goal1),
355 Body1 =.. [search,Goal1|L];
356 builtin(Body) ->
357 Body1 = Body;
358 359 Body =.. L,
360 append(L,AncestorLists,L1),
361 Body1 =.. L1.
362
363ancestor_tests(P,N,Result) :-
364 P == query ->
365 Result = true;
366 367 negated_functor(P,NotP),
368 N2 is N - 2, 369 functor(Head1,P,N2),
370 Head1 =.. [P|Args1],
371 Head2 =.. [NotP|Args1],
372 append(Args1,[PosAncestors,NegAncestors],Args),
373 Head =.. [P|Args],
374 (negative_functor(P) ->
375 C1Ancestors = NegAncestors, C2Ancestors = PosAncestors;
376 377 C1Ancestors = PosAncestors, C2Ancestors = NegAncestors),
378 C1 = (Head :- identical_member(Head1,C1Ancestors), !, fail),
379 count_inferences_pred(IncNcalls),
380 (N2 = 0 -> 381 conjoin((identical_member(Head2,C2Ancestors) , !),IncNcalls,V);
382 383 conjoin(unifiable_member(Head2,C2Ancestors),IncNcalls,V)),
384 (compile_proof_printing ->
385 conjoin(V,infer_by(red),V1);
386 387 V1 = V),
388 C2 = (Head :- V1),
389 conjoin(C1,C2,Result).
390
391procedures_with_ancestor_tests([[P,N]|Preds],Clauses,Procs) :-
392 procedure(P,N,Clauses,Proc1),
393 ancestor_tests(P,N,Tests),
394 conjoin(Tests,Proc1,Proc),
395 procedures_with_ancestor_tests(Preds,Clauses,Procs2),
396 conjoin(Proc,Procs2,Procs).
397procedures_with_ancestor_tests([],_Clauses,true).
398
399identical_member(X,[Y|_]) :- 400 X == Y, 401 !.
402identical_member(X,[_|L]) :-
403 identical_member(X,L).
404
405unifiable_member(X,[Y|_]) :- 406 unify(X,Y). 407unifiable_member(X,[_|L]) :-
408 unifiable_member(X,L).
409
415
416add_proof_recording((Head :- Body),(Head1 :- Body1)) :-
417 Head =.. L,
418 append(L,[Proof,ProofEnd],L1),
419 Head1 =.. L1,
420 add_proof_recording_args(Body,Proof,ProofEnd,Body2),
421 (functor(Head,query,_) ->
422 conjoin(Body2,write_proved(Proof,ProofEnd),Body1);
423 424 Body1 = Body2).
425
426add_proof_recording_args(Body,Proof,ProofEnd,Body1) :-
427 Body = (A , B) ->
428 add_proof_recording_args(A,Proof,Proof1,A1),
429 add_proof_recording_args(B,Proof1,ProofEnd,B1),
430 conjoin(A1,B1,Body1);
431 Body = (A ; B) ->
432 add_proof_recording_args(A,Proof,ProofEnd,A1),
433 add_proof_recording_args(B,Proof,ProofEnd,B1),
434 disjoin(A1,B1,Body1);
435 Body =.. [search,Goal|L] ->
436 add_proof_recording_args(Goal,Proof,ProofEnd,Goal1),
437 Body1 =.. [search,Goal1|L];
438 Body = infer_by(X) ->
439 Body1 = (Proof = [X|ProofEnd]);
440 Body = fail ->
441 Body1 = Body;
442 builtin(Body) ->
443 Proof = ProofEnd,
444 Body1 = Body;
445 446 Body =.. L,
447 append(L,[Proof,ProofEnd],L1),
448 Body1 =.. L1.
449
450write_proved(Proof,ProofEnd) :-
451 write('proved by'),
452 write_proof(Proof,ProofEnd).
453
454write_proof(Proof,ProofEnd) :-
455 Proof == ProofEnd,
456 !.
457write_proof([X|Y],ProofEnd) :-
458 write(' '),
459 write(X),
460 write_proof(Y,ProofEnd).
461
465
466clauses((A , B),L,WffNum) :-
467 !,
468 clauses(A,L1,WffNum),
469 WffNum2 is WffNum + 1,
470 clauses(B,L2,WffNum2),
471 conjoin(L1,L2,L).
472clauses(A,L,WffNum) :-
473 head_literals(A,Lits),
474 clauses(A,Lits,L,WffNum).
475
476clauses(A,[Lit|Lits],L,WffNum) :-
477 body_for_head_literal(Lit,A,Body1),
478 (compile_proof_printing ->
479 conjoin(infer_by(WffNum),Body1,Body);
480 481 Body = Body1),
482 clauses(A,Lits,L1,WffNum),
483 conjoin((Lit :- Body),L1,L).
484clauses(_,[],true,_).
485
486head_literals(Wff,L) :-
487 Wff = (A :- B) -> 488 head_literals(A,L);
489 Wff = (A , B) ->
490 head_literals(A,L1),
491 head_literals(B,L2),
492 union(L1,L2,L);
493 Wff = (A ; B) ->
494 head_literals(A,L1),
495 head_literals(B,L2),
496 union(L1,L2,L);
497 498 L = [Wff].
499
500body_for_head_literal(Head,Wff,Body) :-
501 Wff = (A :- B) ->
502 body_for_head_literal(Head,A,A1),
503 conjoin(A1,B,Body);
504 Wff = (A , B) ->
505 body_for_head_literal(Head,A,A1),
506 body_for_head_literal(Head,B,B1),
507 disjoin(A1,B1,Body);
508 Wff = (A ; B) ->
509 body_for_head_literal(Head,A,A1),
510 body_for_head_literal(Head,B,B1),
511 conjoin(A1,B1,Body);
512 Wff == Head ->
513 Body = true;
514 negated_literal(Wff,Head) ->
515 Body = false;
516 517 negated_literal(Wff,Body).
518
520
521predicates(Wff,L) :-
522 Wff = (A :- B) ->
523 predicates(A,L1),
524 predicates(B,L2),
525 union(L2,L1,L);
526 Wff = (A , B) ->
527 predicates(A,L1),
528 predicates(B,L2),
529 union(L2,L1,L);
530 Wff = (A ; B) ->
531 predicates(A,L1),
532 predicates(B,L2),
533 union(L2,L1,L);
534 functor(Wff,search,_) -> 535 arg(1,Wff,X),
536 predicates(X,L);
537 builtin(Wff) ->
538 L = [];
539 540 functor(Wff,F,N),
541 L = [[F,N]].
542
545
546procedure(P,N,Clauses,Proc) :-
547 Clauses = (A , B) ->
548 procedure(P,N,A,ProcA),
549 procedure(P,N,B,ProcB),
550 conjoin(ProcA,ProcB,Proc);
551 (Clauses = (A :- B) , functor(A,P,N)) ->
552 Proc = Clauses;
553 554 Proc = true.
555
557
558pttp(X) :-
559 time(pttp1(X),'Compilation').
560
561pttp1(X) :-
562 nl,
563 write('PTTP input formulas:'),
564 apply_to_conjuncts(X,write_clause,_),
565 nl,
566 clauses(X,X0,1),
567 apply_to_conjuncts(X0,add_count_inferences,X1),
568 apply_to_conjuncts(X1,add_ancestor,X2),
569 predicates(X2,Preds0),
570 reverse(Preds0,Preds),
571 procedures_with_ancestor_tests(Preds,X2,X3),
572 apply_to_conjuncts(X3,add_sound_unification,X4),
573 apply_to_conjuncts(X4,add_complete_search,X5),
574 (compile_proof_printing ->
575 apply_to_conjuncts(X5,add_proof_recording,Y);
576 577 Y = X5),
578 nl,
579 write('PTTP output formulas:'),
580 apply_to_conjuncts(Y,write_clause,_),
581 nl,
582 nl,
583
584 File = 'temp.prolog', 586
587 open(File,write,OutFile),
588 write_clause_to_file(Y,OutFile),
589 close(OutFile),
590 compile(File),
591 nl,
592 !.
593
594write_clause_to_file((A,B),OutFile) :-
595 write_clause_to_file(A,OutFile),
596 write_clause_to_file(B,OutFile),
597 !.
598write_clause_to_file(A,OutFile) :-
599 nl(OutFile),
600 write(OutFile,A),
601 write(OutFile,.),
602 !.
603
604
605query(M) :- 606 compile_proof_printing ->
607 query(M,_N,_Proof,_ProofEnd);
608 609 query(M,_N).
610
611query :- 612 query(1000000).
613
615
622
623myfunctor(Term,F,N) :-
624 nonvar(F),
625 atomic(F),
626 N == 0,
627 !,
628 Term = F.
629myfunctor(Term,F,N) :-
630 nonvar(Term),
631 atomic(Term),
632 !,
633 F = Term,
634 N = 0.
635myfunctor(Term,F,N) :-
636 functor(Term,F,N).
637
638nop(_).
639
640append([],L,L).
641append([X|L1],L2,[X|L3]) :-
642 append(L1,L2,L3).
643
644reverse([X|L0],L) :-
645 reverse(L0,L1),
646 append(L1,[X],L).
647reverse([],[]).
648
649union([X|L1],L2,L3) :-
650 identical_member(X,L2),
651 !,
652 union(L1,L2,L3).
653union([X|L1],L2,[X|L3]) :-
654 union(L1,L2,L3).
655union([],L,L).
656
657intersection([X|L1],L2,[X|L3]) :-
658 identical_member(X,L2),
659 !,
660 intersection(L1,L2,L3).
661intersection([_X|L1],L2,L3) :-
662 intersection(L1,L2,L3).
663intersection([],_L,[]).
664
670
671conjoin(A,B,C) :-
672 A == true ->
673 C = B;
674 B == true ->
675 C = A;
676 A == false ->
677 C = false;
678 B == false ->
679 C = false;
680 681 C = (A , B).
682
683disjoin(A,B,C) :-
684 A == true ->
685 C = true;
686 B == true ->
687 C = true;
688 A == false ->
689 C = B;
690 B == false ->
691 C = A;
692 693 C = (A ; B).
694
695negated_functor(F,NotF) :-
696 name(F,L),
697 name(not_,L1),
698 (append(L1,L2,L) ->
699 true;
700 701 append(L1,L,L2)),
702 name(NotF,L2).
703
704negated_literal(Lit,NotLit) :-
705 Lit =.. [F1|L1],
706 negated_functor(F1,F2),
707 (var(NotLit) ->
708 NotLit =.. [F2|L1];
709 710 NotLit =.. [F2|L2],
711 L1 == L2).
712
713negative_functor(F) :-
714 name(F,L),
715 name(not_,L1),
716 append(L1,_,L).
717
718negative_literal(Lit) :-
719 functor(Lit,F,_),
720 negative_functor(F).
721
722apply_to_conjuncts(Wff,P,Wff1) :-
723 Wff = (A , B) ->
724 apply_to_conjuncts(A,P,A1),
725 apply_to_conjuncts(B,P,B1),
726 conjoin(A1,B1,Wff1);
727 728 T1 =.. [P,Wff,Wff1],
729 call(T1).
730
731write_clause(A) :-
732 nl,
733 write(A),
734 write(.).
735
736write_clause(A,_) :- 737 write_clause(A). 738
745
746count_inferences :- 747 retract(count_inferences_pred(_)), 748 fail.
749count_inferences :-
750 assert(count_inferences_pred(inc_ncalls)).
751
752dont_count_inferences :- 753 retract(count_inferences_pred(_)), 754 fail.
755dont_count_inferences :-
756 assert(count_inferences_pred(true)).
757
758:- dont_count_inferences. 759
761
762add_count_inferences((Head :- Body),(Head :- Body1)) :-
763 functor(Head,query,_) ->
764 Body1 = Body;
765 766 count_inferences_pred(P),
767 conjoin(P,Body,Body1).
768
769clear_ncalls :-
770 retract(ncalls(_)),
771 fail.
772clear_ncalls :-
773 assert(ncalls(0)).
774
775inc_ncalls :-
776 retract(ncalls(N)),
777 N1 is N + 1,
778 assert(ncalls(N1)),
779 !.
780
783
784trace_search :- 785 retract(trace_search_progress_pred(_)),
786 fail.
787trace_search :-
788 assert(trace_search_progress_pred(write_search_progress)).
789
790dont_trace_search :- 791 retract(trace_search_progress_pred(_)),
792 fail.
793dont_trace_search :-
794 assert(trace_search_progress_pred(nop)).
795
796:- trace_search. 797
798write_search_progress(Level) :-
799 ncalls(N),
800 (N > 0 -> write(N) , write(' inferences so far.') ; true),
801 nl,
802 write('Begin cost '),
803 write(Level),
804 write(' search... ').
805
811
812print_proof :- 813 retract(compile_proof_printing),
814 fail.
815print_proof :-
816 assert(compile_proof_printing).
817
818dont_print_proof :- 819 retract(compile_proof_printing),
820 fail.
821dont_print_proof.
822
823:- print_proof. 824
826
827time(X) :-
828 time(X,'Execution').
829
830time(X,Type) :-
831 clear_ncalls,
832
833 statistics(runtime,[T1,_]), 835
836 call(X),
837
838 statistics(runtime,[T2,_]), 839 Secs is (T2 - T1) / 1000.0, 842
843 nl,
844 write(Type),
845 write(' time: '),
846 ncalls(N),
847 (N > 0 -> write(N) , write(' inferences in ') ; true),
848 write(Secs),
849 write(' seconds, including printing'),
850 nl.
851
858
859builtin(T) :-
860 functor(T,F,N),
861 builtin(F,N).
862
863builtin(!,0).
864builtin(true,0).
865builtin(fail,0).
866builtin(succeed,0).
867builtin(trace,0).
868builtin(atom,1).
869builtin(integer,1).
870builtin(number,1).
871builtin(atomic,1).
872builtin(constant,1).
873builtin(functor,3).
874builtin(arg,3).
875builtin(var,1).
876builtin(nonvar,1).
877builtin(call,1).
878builtin(=,2).
879builtin(\=,2).
880builtin(==,2).
881builtin(\==,2).
882builtin(>,2).
883builtin(<,2).
884builtin(>=,2).
885builtin(=<,2).
886builtin(is,2).
887builtin(display,1).
888builtin(write,1).
889builtin(nl,0).
890builtin(infer_by,_).
891builtin(write_proved,_).
892builtin(search,_).
893builtin(search_cost,_).
894builtin(unify,_).
895builtin(identical_member,_).
896builtin(unifiable_member,_).
897builtin(inc_ncalls,0).
898
903
908
909chang_lee_example2 :-
910 nl,
911 write(chang_lee_example2),
912 pttp((
913 p(e,X,X),
914 p(X,e,X),
915 p(X,X,e),
916 p(a,b,c),
917 (p(U,Z,W) :- p(X,Y,U) , p(Y,Z,V) , p(X,V,W)),
918 (p(X,V,W) :- p(X,Y,U) , p(Y,Z,V) , p(U,Z,W)),
919 (query :- search(p(b,a,c)))
920 )),
921 time(query).
922
923chang_lee_example8 :-
924 nl,
925 write(chang_lee_example8),
926 pttp((
927 l(1,a),
928 d(X,X),
929 (p(X) ; d(g(X),X)),
930 (p(X) ; l(1,g(X))),
931 (p(X) ; l(g(X),X)),
932 (not_p(X) ; not_d(X,a)),
933 (not_d(X,Y) ; not_d(Y,Z) ; d(X,Z)),
934 (not_l(1,X) ; not_l(X,a) ; p(f(X))),
935 (not_l(1,X) ; not_l(X,a) ; d(f(X),X)),
936 (query :- (p(X) , d(X,a)))
937 )),
938 time(search(query))