- From: Yosi Scharf <syosi@MIT.EDU>
- Date: Mon, 23 May 2005 23:39:52 -0400
- To: public-cwm-bugs@w3.org
- Message-ID: <4292A208.7060506@mit.edu>
I was trying to implement the lambda calculus in n3.
This is because as far as I can tell, it can be done.
However, I am getting internal cwm errors when trying to run it.
the file is http://www.w3.org/2000/10/swap/test/turing/lambda.n3
so.
[syosi@yosi turing]$ cwm
http://www.w3.org/2000/10/swap/test/turing/lambda.n3 --think
#Processed by Id: cwm.py,v 1.167 2005/01/10 19:15:22 syosi Exp
# using base http://www.w3.org/2000/10/swap/test/turing/lambda.n3
@@@ Not in existentials or variables but now bound: li71
Traceback (most recent call last):
File "/home/syosi/SWAP/cwm.py", line 652, in ?
doCommand()
File "/home/syosi/SWAP/cwm.py", line 563, in doCommand
think(workingContext, mode=option_flags["think"])
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 62, in think
return InferenceTask(knowledgeBase, ruleFormula, mode=mode,
repeat=1).run()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 222, in run
return self.runSmart()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 210, in
runSmart
total += cy.run()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 351, in run
found = rule.once()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 443, in once
total = query.resolve()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 587, in
resolve
return self.unify(self.queue, self.variables, self.existentials)
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 827, in unify
bindings.copy(), nb, evidence = evidence + [reason])
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 827, in unify
bindings.copy(), nb, evidence = evidence + [reason])
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 715, in unify
existentials.remove(pair[0]) # Can't match anything anymore, need
exact match
KeyError: li71
This is not what I expected. Note that that outlup is from cwm cvs, not
cwm 1.0.
attached is the result of running cwm
http://www.w3.org/2000/10/swap/test/turing/lambda.n3 --chatty=1000
--think 2>&1 | cat > /tmp/cwm.log
I don't have time to analyze what is happening now. It's late.
Yosi
think: rules from {12} added to {12}
New Inference task, rules from {12}
----occuringIn: {3}
----occuringIn: {li2 binds B}
New Rule R1 ============ looking for:
{{3}:: li2 rdf:type NeedsFindBinding}
{{3}:: E rdf:first li4}
{{3}:: E rdf:rest R}
=>
{{li2 binds B}:: li2 binds B}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template R,E,X,B
also used in conclusion E,X,B
Existentials in template R
Found rule R1 for statement {{12}:: {3} implies {li2 binds B}}
----occuringIn: {3}
----occuringIn: {li7 rdf:type NeedsFindBinding}
New Rule R2 ============ looking for:
{{3}:: li2 rdf:type NeedsFindBinding}
{{3}:: E rdf:first li5}
{{3}:: E rdf:rest R}
=>
{{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template R,E,X,A,B
also used in conclusion R,X
Existentials in template A,E,B
Found rule R2 for statement {{12}:: {3} implies {li7 rdf:type NeedsFindBinding}}
----occuringIn: {li12 rdf:type NeedsEval}
----occuringIn: {li12 eval li15}
New Rule R3 ============ looking for:
{{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval}
=>
{{li12 eval li15}:: li12 eval li15}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template Y,X,E
also used in conclusion E,X,Y
Existentials in template
Found rule R3 for statement {{12}:: {li12 rdf:type NeedsEval} implies {li12 eval li15}}
----occuringIn: {li2 rdf:type NeedsEval}
----occuringIn: {li2 rdf:type NeedsFindBinding}
New Rule R4 ============ looking for:
{{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval}
=>
{{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template E,X
also used in conclusion E,X
Existentials in template
Found rule R4 for statement {{12}:: {li2 rdf:type NeedsEval} implies {li2 rdf:type NeedsFindBinding}}
----occuringIn: {2}
----occuringIn: {li2 eval R}
New Rule R5 ============ looking for:
{{2}:: li2 rdf:type NeedsEval}
{{2}:: li2 binds R}
=>
{{li2 eval R}:: li2 eval R}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template X,E,R
also used in conclusion E,X,R
Existentials in template
Found rule R5 for statement {{12}:: {2} implies {li2 eval R}}
----occuringIn: {li17 rdf:type NeedsEval}
----occuringIn: {li17 eval li15}
New Rule R6 ============ looking for:
{{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval}
=>
{{li17 eval li15}:: li17 eval li15}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template X,Y,F,E
also used in conclusion E,F,Y,X
Existentials in template
Found rule R6 for statement {{12}:: {li17 rdf:type NeedsEval} implies {li17 eval li15}}
----occuringIn: {li18 rdf:type NeedsEval}
----occuringIn: {2}
New Rule R7 ============ looking for:
{{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval}
=>
{{2}:: li19 rdf:type NeedsEval}
{{2}:: li20 rdf:type NeedsEval}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template B,A,E
also used in conclusion A,E,B
Existentials in template
Found rule R7 for statement {{12}:: {li18 rdf:type NeedsEval} implies {2}}
----occuringIn: {3}
----occuringIn: {li21 rdf:type NeedsApply}
New Rule R8 ============ looking for:
{{3}:: li18 rdf:type NeedsEval}
{{3}:: li19 eval F}
{{3}:: li20 eval X}
=>
{{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template F,X,E,A,B
also used in conclusion X,F
Existentials in template A,E,B
Found rule R8 for statement {{12}:: {3} implies {li21 rdf:type NeedsApply}}
----occuringIn: {li23 rdf:type NeedsApply}
----occuringIn: {3}
New Rule R9 ============ looking for:
{{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply}
=>
{{3}:: _g_L89C6 rdf:first li24}
{{3}:: _g_L89C6 rdf:rest E}
{{3}:: li26 rdf:type NeedsEval}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template X,Y,A,E
also used in conclusion X,A,Y,E
Existentials in template
Found rule R9 for statement {{12}:: {li23 rdf:type NeedsApply} implies {3}}
----occuringIn: {X rdf:type NeedsRun}
----occuringIn: {li28 rdf:type NeedsEval}
New Rule R10 ============ looking for:
{{X rdf:type NeedsRun}:: X rdf:type NeedsRun}
=>
{{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template X
also used in conclusion X
Existentials in template
Found rule R10 for statement {{12}:: {X rdf:type NeedsRun} implies {li28 rdf:type NeedsEval}}
----occuringIn: {2}
----occuringIn: {X results R}
New Rule R11 ============ looking for:
{{2}:: li28 eval R}
{{2}:: X rdf:type NeedsRun}
=>
{{X results R}:: X results R}
Universals declared in outer B,F,A,E,Y,X,R
mentioned in template X,R
also used in conclusion R,X
Existentials in template
Found rule R11 for statement {{12}:: {2} implies {X results R}}
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
R1 can affect R5 because {{li2 binds B}:: li2 binds B} can trigger {{2}:: li2 binds R}
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{3}:: li20 eval X} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{li2 binds B}:: li2 binds B} {{2}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{2}:: li2 binds R} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
R3 can affect R8 because {{li12 eval li15}:: li12 eval li15} can trigger {{3}:: li19 eval F}
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{li12 eval li15}:: li12 eval li15} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
R3 can affect R11 because {{li12 eval li15}:: li12 eval li15} can trigger {{2}:: li28 eval R}
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{2}:: li2 binds R} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
R5 can affect R8 because {{li2 eval R}:: li2 eval R} can trigger {{3}:: li19 eval F}
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{li2 eval R}:: li2 eval R} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
R5 can affect R11 because {{li2 eval R}:: li2 eval R} can trigger {{2}:: li28 eval R}
R2 can affect R1 because {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} can trigger {{3}:: li2 rdf:type NeedsFindBinding}
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 3
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{2}:: li2 binds R} 1
R2* can affect R2* because {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} can trigger {{3}:: li2 rdf:type NeedsFindBinding}
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 3
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 3
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{3}:: li20 eval X} 1
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 3
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 3
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li7 rdf:type NeedsFindBinding}:: li7 rdf:type NeedsFindBinding} {{2}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{2}:: li2 binds R} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
R6 can affect R8 because {{li17 eval li15}:: li17 eval li15} can trigger {{3}:: li19 eval F}
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{li17 eval li15}:: li17 eval li15} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
R6 can affect R11 because {{li17 eval li15}:: li17 eval li15} can trigger {{2}:: li28 eval R}
R4 can affect R1 because {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} can trigger {{3}:: li2 rdf:type NeedsFindBinding}
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 3
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{2}:: li2 binds R} 1
R4 can affect R2* because {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} can trigger {{3}:: li2 rdf:type NeedsFindBinding}
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 3
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 3
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{3}:: li20 eval X} 1
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 3
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 3
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li2 rdf:type NeedsFindBinding}:: li2 rdf:type NeedsFindBinding} {{2}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 3
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{2}:: li2 binds R} 1
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 3
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 3
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{3}:: li20 eval X} 1
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 3
R8 can affect R9 because {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} can trigger {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply}
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li21 rdf:type NeedsApply}:: li21 rdf:type NeedsApply} {{2}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{2}:: li19 rdf:type NeedsEval} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{2}:: li20 rdf:type NeedsEval} {{3}:: E rdf:rest R} 1
R7 can affect R3 because {{2}:: li19 rdf:type NeedsEval} can trigger {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval}
R7 can affect R5 because {{2}:: li19 rdf:type NeedsEval} can trigger {{2}:: li2 rdf:type NeedsEval}
...couldn't beccause of {{2}:: li19 rdf:type NeedsEval} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{2}:: li20 rdf:type NeedsEval} {{3}:: E rdf:rest R} 1
R7 can affect R6 because {{2}:: li19 rdf:type NeedsEval} can trigger {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval}
R7 can affect R4 because {{2}:: li19 rdf:type NeedsEval} can trigger {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval}
R7 can affect R8 because {{2}:: li19 rdf:type NeedsEval} can trigger {{3}:: li18 rdf:type NeedsEval}
R7* can affect R7* because {{2}:: li19 rdf:type NeedsEval} can trigger {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval}
...couldn't beccause of {{2}:: li19 rdf:type NeedsEval} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 3
...couldn't beccause of {{2}:: li20 rdf:type NeedsEval} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 3
...couldn't beccause of {{2}:: li19 rdf:type NeedsEval} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{2}:: li20 rdf:type NeedsEval} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{2}:: li19 rdf:type NeedsEval} {{2}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{2}:: li20 rdf:type NeedsEval} {{2}:: X rdf:type NeedsRun} 3
R9 can affect R1 because {{3}:: _g_L89C6 rdf:first li24} can trigger {{3}:: E rdf:first li4}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
R9 can affect R3 because {{3}:: li26 rdf:type NeedsEval} can trigger {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{2}:: li2 binds R} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{2}:: li2 binds R} 1
R9 can affect R5 because {{3}:: li26 rdf:type NeedsEval} can trigger {{2}:: li2 rdf:type NeedsEval}
R9 can affect R2* because {{3}:: _g_L89C6 rdf:first li24} can trigger {{3}:: E rdf:first li5}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
R9 can affect R6 because {{3}:: li26 rdf:type NeedsEval} can trigger {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
R9 can affect R4 because {{3}:: li26 rdf:type NeedsEval} can trigger {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{3}:: li20 eval X} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{3}:: li20 eval X} 1
R9 can affect R8 because {{3}:: li26 rdf:type NeedsEval} can trigger {{3}:: li18 rdf:type NeedsEval}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
R9 can affect R7* because {{3}:: li26 rdf:type NeedsEval} can trigger {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval}
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{3}:: li26 rdf:type NeedsEval} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 3
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{3}:: li26 rdf:type NeedsEval} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{3}:: _g_L89C6 rdf:first li24} {{2}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{3}:: _g_L89C6 rdf:rest E} {{2}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{3}:: li26 rdf:type NeedsEval} {{2}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} {{3}:: E rdf:rest R} 1
R10 can affect R3 because {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} can trigger {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval}
R10 can affect R5 because {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} can trigger {{2}:: li2 rdf:type NeedsEval}
...couldn't beccause of {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} {{3}:: E rdf:rest R} 1
R10 can affect R6 because {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} can trigger {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval}
R10 can affect R4 because {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} can trigger {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval}
R10 can affect R8 because {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} can trigger {{3}:: li18 rdf:type NeedsEval}
R10 can affect R7* because {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} can trigger {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval}
...couldn't beccause of {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 3
...couldn't beccause of {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{li28 rdf:type NeedsEval}:: li28 rdf:type NeedsEval} {{2}:: X rdf:type NeedsRun} 3
...couldn't beccause of {{X results R}:: X results R} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{X results R}:: X results R} {{li12 rdf:type NeedsEval}:: li12 rdf:type NeedsEval} 1
...couldn't beccause of {{X results R}:: X results R} {{2}:: li2 binds R} 1
...couldn't beccause of {{X results R}:: X results R} {{3}:: E rdf:rest R} 1
...couldn't beccause of {{X results R}:: X results R} {{li17 rdf:type NeedsEval}:: li17 rdf:type NeedsEval} 1
...couldn't beccause of {{X results R}:: X results R} {{li2 rdf:type NeedsEval}:: li2 rdf:type NeedsEval} 1
...couldn't beccause of {{X results R}:: X results R} {{3}:: li20 eval X} 1
...couldn't beccause of {{X results R}:: X results R} {{li18 rdf:type NeedsEval}:: li18 rdf:type NeedsEval} 1
...couldn't beccause of {{X results R}:: X results R} {{li23 rdf:type NeedsApply}:: li23 rdf:type NeedsApply} 1
...couldn't beccause of {{X results R}:: X results R} {{X rdf:type NeedsRun}:: X rdf:type NeedsRun} 1
...couldn't beccause of {{X results R}:: X results R} {{2}:: X rdf:type NeedsRun} 1
Aff: R1 R3 R5 R2* R6 R4 R8 R7* R9 R10 R11
R1: - - - X - X - - X -
R3: - - - - - - - X X X
R5: X - - - - - - X X X
R2*: - - - X - X - - X -
R6: - - - - - - - X X X
R4: - - - - - - - X X X
R8: - X X - X - - X X X
R7*: - - - - - - - X X X
R9: - - - - - - X - - -
R10:
R11: - X X - X - - - - -
R1 indirectly affects [R1, R2*, R3, R4, R5, R6, R7*, R8, R9, R11] and is affected by [R1, R2*, R3, R4, R5, R6, R7*, R8, R9, R10]
New cyclic: [R1, R2*, R3, R4, R5, R6, R7*, R8, R9]
New cyclic: [R10]
New cyclic: [R11]
partial topo: [[R11]]
partial topo: [[R1, R2*, R3, R4, R5, R6, R7*, R8, R9], [R11]]
partial topo: [[R10]]
In order:[[R10], [R1, R2*, R3, R4, R5, R6, R7*, R8, R9], [R11]]
Running cyclic system [R10]
Trying rule R10 ===================
{12} :: X rdf:type NeedsRun.
Query: created with 1 terms. (justone=0, wc={12})
{12} :: X rdf:type NeedsRun.
Smart in: [{12}]
rdf:type needs to run: set([])
X needs to run: set([X])
NeedsRun needs to run: set([])
setup: 60) short=1, {12}(et([]) :: X(et([X])? rdf:type(et([]) NeedsRun(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
60) short=1, {12}(et([]) :: X(et([X])? rdf:type(et([]) NeedsRun(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
60) short=1, {12}(et([]) :: X(et([X])? rdf:type(et([]) NeedsRun(et([]).
Looking at 60) short=1, {12}(et([]) :: X(et([X])? rdf:type(et([]) NeedsRun(et([]).
...with vars(X) ExQuVars:()
Searching (S=60) 1 for 60) short=1, {12}(et([]) :: X(et([X])? rdf:type(et([]) NeedsRun(et([]).
...checking {{12}:: li38 rdf:type NeedsRun}
nb1 = {X: li38}
nb = {}
...searchDone, now 80) short=1, {12}(et([]) :: X(et([X])? rdf:type(et([]) NeedsRun(et([]).
nbs=[({X: li38}, {{12}:: li38 rdf:type NeedsRun})]
QUERY2: called 0 terms, 0 bindings {}, (new: {X: li38})
new binding: X -> li38
QUERY MATCH COMPLETE with bindings: {X: li38}
Concluding tentatively...{X: li38}
Not duplicate: {X: li38}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY {li28 rdf:type NeedsEval}->{12} X->li38
Substition of variables {X: li38, {li28 rdf:type NeedsEval}: {12}} in list li28
...yields NEW li39 = [[[lambda, [x], x], [lambda, [y], [y, y]]], []]
SubstituteEquals list li39 with {}
Add statement (size before 127, 12 statements) to {12}:
{li39 rdf:type NeedsEval}
Added 1, nominal size of store changed from 127 to 128.
Nested query returns 1 fo {X: li38}
Item state 80, returning total 1
Rule try generated 1 new statements
Running cyclic system [R1, R2*, R3, R4, R5, R6, R7*, R8, R9]
Trying rule R1 ===================
{13} :: li2 rdf:type NeedsFindBinding.
{13} :: E rdf:first li4.
{13} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={13})
{13} :: li2 rdf:type NeedsFindBinding.
{13} :: E rdf:first li4.
{13} :: E rdf:rest R.
Smart in: [{13}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
...searchDone, now 80) short=0, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
setup: 80) short=0, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
match: abandoned, no way for 80) short=0, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
Rule try generated 0 new statements
Rule R1 gave 0. Affects:[R5].
Trying rule R2* ===================
{13} :: li2 rdf:type NeedsFindBinding.
{13} :: E rdf:first li5.
{13} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={13})
{13} :: li2 rdf:type NeedsFindBinding.
{13} :: E rdf:first li5.
{13} :: E rdf:rest R.
Smart in: [{13}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
...searchDone, now 80) short=0, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
setup: 80) short=0, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
match: abandoned, no way for 80) short=0, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
Rule try generated 0 new statements
Rule R2* gave 0. Affects:[R1, R2*].
Trying rule R3 ===================
{13} :: li12 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={13})
{13} :: li12 rdf:type NeedsEval.
Smart in: [{13}]
rdf:type needs to run: set([])
li12 needs to run: set([Y, X, E])
NeedsEval needs to run: set([])
setup: 45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(X,E,Y) ExQuVars:()
Searching (S=45) 1 for 45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{13}:: li39 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with li31 vars=set([X, E, Y]), so far={}
Searching deep 45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=1, {13}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R3 gave 0. Affects:[R8].
Trying rule R4 ===================
{13} :: li2 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={13})
{13} :: li2 rdf:type NeedsEval.
Smart in: [{13}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsEval needs to run: set([])
setup: 45) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
...with vars(X,E) ExQuVars:()
Searching (S=45) 1 for 45) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
...checking {{13}:: li39 rdf:type NeedsEval}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E]), so far={}
Unifying symbol X with li38 vars=set([X, E]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E]), so far={X: li38}
Unifying symbol E with () vars=set([E]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...searchDone, now 80) short=1, {13}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), X: li38}, {{13}:: li39 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li38})
new binding: E -> ()
new binding: X -> li38
QUERY MATCH COMPLETE with bindings: {X: li38, E: ()}
Concluding tentatively...{X: li38, E: ()}
Not duplicate: {X: li38, E: ()}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY E->() X->li38 {li2 rdf:type NeedsFindBinding}->{13}
Substition of variables {X: li38, E: (), {li2 rdf:type NeedsFindBinding}: {13}} in list li2
...yields NEW li39 = [[[lambda, [x], x], [lambda, [y], [y, y]]], []]
SubstituteEquals list li39 with {}
Add statement (size before 128, 13 statements) to {13}:
{li39 rdf:type NeedsFindBinding}
Added 1, nominal size of store changed from 128 to 129.
Nested query returns 1 fo {E: (), X: li38}
Item state 80, returning total 1
Rule try generated 1 new statements
Rule R4 gave 1. Affects:[R1, R2*].
...rescheduling R1
...rescheduling R2*
Trying rule R5 ===================
{14} :: li2 rdf:type NeedsEval.
{14} :: li2 binds R.
Query: created with 2 terms. (justone=0, wc={14})
{14} :: li2 rdf:type NeedsEval.
{14} :: li2 binds R.
Smart in: [{14}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsEval needs to run: set([])
setup: 45) short=1, {14}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
binds needs to run: set([])
li2 needs to run: set([E, X])
R needs to run: set([R])
...searchDone, now 80) short=0, {14}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
setup: 80) short=0, {14}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
match: abandoned, no way for 80) short=0, {14}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
Rule try generated 0 new statements
Rule R5 gave 0. Affects:[R8].
Trying rule R6 ===================
{14} :: li17 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={14})
{14} :: li17 rdf:type NeedsEval.
Smart in: [{14}]
rdf:type needs to run: set([])
li17 needs to run: set([X, Y, F, E])
NeedsEval needs to run: set([])
setup: 45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(F,X,E,Y) ExQuVars:()
Searching (S=45) 1 for 45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{14}:: li39 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with li31 vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=1, {14}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R6 gave 0. Affects:[R8].
Trying rule R7* ===================
{14} :: li18 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={14})
{14} :: li18 rdf:type NeedsEval.
Smart in: [{14}]
rdf:type needs to run: set([])
li18 needs to run: set([B, A, E])
NeedsEval needs to run: set([])
setup: 45) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(E,A,B) ExQuVars:()
Searching (S=45) 1 for 45) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{14}:: li39 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([E, A, B]), so far={}
Unifying symbol A with li31 vars=set([E, A, B]), so far={}
Unifying term MATCHED A to li31
Unifying list [B] with [[lambda, [y], [y, y]]] vars=set([E, B]), so far={A: li31}
Unifying symbol B with li36 vars=set([E, B]), so far={A: li31}
Unifying term MATCHED B to li36
Unifying list [E] with [[]] vars=set([E]), so far={B: li36, A: li31}
Unifying symbol E with () vars=set([E]), so far={B: li36, A: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({A: li31, E: (), B: li36}, None)]
nb1 = {A: li31, E: (), B: li36}
nb = {}
...searchDone, now 80) short=1, {14}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), A: li31, B: li36}, {{14}:: li39 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), A: li31, B: li36})
new binding: E -> ()
new binding: A -> li31
new binding: B -> li36
QUERY MATCH COMPLETE with bindings: {A: li31, E: (), B: li36}
Concluding tentatively...{A: li31, E: (), B: li36}
Not duplicate: {A: li31, E: (), B: li36}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY {2}->{14} E->() A->li31 B->li36
Substition of variables {E: (), {2}: {14}, A: li31, B: li36} in list li19
...yields NEW li40 = [[lambda, [x], x], []]
SubstituteEquals list li40 with {}
Add statement (size before 129, 14 statements) to {14}:
{li40 rdf:type NeedsEval}
Substition of variables {E: (), {2}: {15}, A: li31, B: li36} in list li20
...yields NEW li41 = [[lambda, [y], [y, y]], []]
SubstituteEquals list li41 with {}
Add statement (size before 130, 15 statements) to {15}:
{li41 rdf:type NeedsEval}
Added 2, nominal size of store changed from 129 to 131.
Nested query returns 2 fo {E: (), A: li31, B: li36}
Item state 80, returning total 2
Rule try generated 2 new statements
Rule R7* gave 2. Affects:[R3, R4, R5, R6, R7*, R8].
...rescheduling R3
...rescheduling R4
...rescheduling R5
...rescheduling R6
...rescheduling R7*
Trying rule R8 ===================
{16} :: li18 rdf:type NeedsEval.
{16} :: li19 eval F.
{16} :: li20 eval X.
Query: created with 3 terms. (justone=0, wc={16})
{16} :: li18 rdf:type NeedsEval.
{16} :: li19 eval F.
{16} :: li20 eval X.
Smart in: [{16}]
rdf:type needs to run: set([])
li18 needs to run: set([B, A, E])
NeedsEval needs to run: set([])
setup: 45) short=3, {16}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
eval needs to run: set([])
li19 needs to run: set([E, A])
F needs to run: set([F])
...searchDone, now 80) short=0, {16}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
setup: 80) short=0, {16}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
match: abandoned, no way for 80) short=0, {16}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
Rule try generated 0 new statements
Rule R8 gave 0. Affects:[R9].
Trying rule R9 ===================
{16} :: li23 rdf:type NeedsApply.
Query: created with 1 terms. (justone=0, wc={16})
{16} :: li23 rdf:type NeedsApply.
Smart in: [{16}]
rdf:type needs to run: set([])
li23 needs to run: set([X, Y, A, E])
NeedsApply needs to run: set([])
...searchDone, now 80) short=0, {16}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
setup: 80) short=0, {16}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
match: abandoned, no way for 80) short=0, {16}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
Rule try generated 0 new statements
Rule R9 gave 0. Affects:[R1, R2*, R3, R4, R5, R6, R7*, R8].
Trying rule R1 ===================
{16} :: li2 rdf:type NeedsFindBinding.
{16} :: E rdf:first li4.
{16} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={16})
{16} :: li2 rdf:type NeedsFindBinding.
{16} :: E rdf:first li4.
{16} :: E rdf:rest R.
Smart in: [{16}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li4 needs to run: set([B, X])
setup: 50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...searchDone, now 30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
Looking at 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,E,B) ExQuVars:(R)
Searching (S=45) 1 for 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{16}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li38 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li38}
Unifying symbol E with () vars=set([E, B]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...searchDone, now 80) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{16}:: li39 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {16}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li38}
Substition of variables {E: (), X: li38} in list li4
...yields NEW li42 = [[[lambda, [x], x], [lambda, [y], [y, y]]], B]
...bound becomes 65) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
query iterating with 2 terms, 2 bindings: X->li38 E->() ; 2 new bindings: E->() X->li38 .
65) short=7730, {16}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
Looking at 65) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R1 gave 0. Affects:[R5].
Trying rule R2* ===================
{16} :: li2 rdf:type NeedsFindBinding.
{16} :: E rdf:first li5.
{16} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={16})
{16} :: li2 rdf:type NeedsFindBinding.
{16} :: E rdf:first li5.
{16} :: E rdf:rest R.
Smart in: [{16}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li5 needs to run: set([B, A])
setup: 50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=50) 0 for 50) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=50) 0 for 50) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
...searchDone, now 30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
Looking at 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=45) 1 for 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{16}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, R]), so far={}
Unifying symbol X with li38 vars=set([X, R]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([R]), so far={X: li38}
Unifying symbol E with () vars=set([R]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...searchDone, now 80) short=1, {16}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{16}:: li39 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {16}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {16}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {16}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li38 ; 2 new bindings: E->() X->li38 .
65) short=7730, {16}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {16}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R2* gave 0. Affects:[R1, R2*].
Trying rule R3 ===================
{16} :: li12 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={16})
{16} :: li12 rdf:type NeedsEval.
Smart in: [{16}]
rdf:type needs to run: set([])
li12 needs to run: set([Y, X, E])
NeedsEval needs to run: set([])
setup: 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(X,E,Y) ExQuVars:()
Searching (S=45) 3 for 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{16}:: li39 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with li31 vars=set([X, E, Y]), so far={}
Searching deep 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{16}:: li40 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[lambda, [x], x], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [lambda, [x], x] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with lambda vars=set([X, E, Y]), so far={}
Unifying list [[X], Y] with [[x], x] vars=set([E, X, Y]), so far={}
Unifying list [X] with [x] vars=set([E, X, Y]), so far={}
Unifying symbol X with x vars=set([E, X, Y]), so far={}
Unifying term MATCHED X to x
Unifying list [Y] with [x] vars=set([E, Y]), so far={X: x}
Unifying symbol Y with x vars=set([E, Y]), so far={X: x}
Unifying term MATCHED Y to x
Unifying list [E] with [[]] vars=set([E]), so far={X: x, Y: x}
Unifying symbol E with () vars=set([E]), so far={X: x, Y: x}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({Y: x, E: (), X: x}, None)]
nb1 = {Y: x, E: (), X: x}
nb = {}
...checking {{16}:: li41 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[lambda, [y], [y, y]], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [lambda, [y], [y, y]] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with lambda vars=set([X, E, Y]), so far={}
Unifying list [[X], Y] with [[y], [y, y]] vars=set([E, X, Y]), so far={}
Unifying list [X] with [y] vars=set([E, X, Y]), so far={}
Unifying symbol X with y vars=set([E, X, Y]), so far={}
Unifying term MATCHED X to y
Unifying list [Y] with [[y, y]] vars=set([E, Y]), so far={X: y}
Unifying symbol Y with li33 vars=set([E, Y]), so far={X: y}
Unifying term MATCHED Y to li33
Unifying list [E] with [[]] vars=set([E]), so far={X: y, Y: li33}
Unifying symbol E with () vars=set([E]), so far={X: y, Y: li33}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({Y: li33, E: (), X: y}, None)]
nb1 = {Y: li33, E: (), X: y}
nb = {}
...searchDone, now 80) short=3, {16}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), Y: x, X: x}, {{16}:: li40 rdf:type NeedsEval}), ({E: (), Y: li33, X: y}, {{16}:: li41 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), Y: x, X: x})
new binding: E -> ()
new binding: Y -> x
new binding: X -> x
QUERY MATCH COMPLETE with bindings: {Y: x, E: (), X: x}
Concluding tentatively...{Y: x, E: (), X: x}
Not duplicate: {Y: x, E: (), X: x}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY E->() Y->x {li12 eval li15}->{16} X->x
Substition of variables {Y: x, E: (), {li12 eval li15}: {16}, X: x} in list li8
...yields NEW li29 = [x]
Substition of variables {Y: x, E: (), {li12 eval li15}: {16}, X: x} in list li11
...yields NEW li31 = [lambda, [x], x]
Substition of variables {Y: x, E: (), {li12 eval li15}: {16}, X: x} in list li12
...yields NEW li40 = [[lambda, [x], x], []]
Substition of variables {Y: x, E: (), {li12 eval li15}: {16}, X: x} in list li15
...yields NEW li45 = [function, x, x, []]
SubstituteEquals list li40 with {}
SubstituteEquals list li45 with {}
Add statement (size before 131, 16 statements) to {16}:
{li40 eval li45}
Added 1, nominal size of store changed from 131 to 132.
Nested query returns 1 fo {E: (), Y: x, X: x}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), Y: li33, X: y})
new binding: E -> ()
new binding: Y -> li33
new binding: X -> y
QUERY MATCH COMPLETE with bindings: {Y: li33, E: (), X: y}
Concluding tentatively...{Y: li33, E: (), X: y}
Not duplicate: {Y: li33, E: (), X: y}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY E->() Y->li33 {li12 eval li15}->{17} X->y
Substition of variables {Y: li33, E: (), {li12 eval li15}: {17}, X: y} in list li8
...yields NEW li32 = [y]
Substition of variables {Y: li33, E: (), {li12 eval li15}: {17}, X: y} in list li11
...yields NEW li36 = [lambda, [y], [y, y]]
Substition of variables {Y: li33, E: (), {li12 eval li15}: {17}, X: y} in list li12
...yields NEW li41 = [[lambda, [y], [y, y]], []]
Substition of variables {Y: li33, E: (), {li12 eval li15}: {17}, X: y} in list li15
...yields NEW li48 = [function, y, [y, y], []]
SubstituteEquals list li41 with {}
SubstituteEquals list li48 with {}
Add statement (size before 132, 17 statements) to {17}:
{li41 eval li48}
Added 1, nominal size of store changed from 132 to 133.
Nested query returns 1 fo {E: (), Y: li33, X: y}
Item state 80, returning total 2
Rule try generated 2 new statements
Rule R3 gave 2. Affects:[R8].
...rescheduling R8
Trying rule R4 ===================
{18} :: li2 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={18})
{18} :: li2 rdf:type NeedsEval.
Smart in: [{18}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsEval needs to run: set([])
setup: 45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
...with vars(X,E) ExQuVars:()
Searching (S=45) 3 for 45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
...checking {{18}:: li39 rdf:type NeedsEval}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E]), so far={}
Unifying symbol X with li38 vars=set([X, E]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E]), so far={X: li38}
Unifying symbol E with () vars=set([E]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{18}:: li40 rdf:type NeedsEval}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, E]), so far={}
Unifying symbol X with li31 vars=set([X, E]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([E]), so far={X: li31}
Unifying symbol E with () vars=set([E]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{18}:: li41 rdf:type NeedsEval}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, E]), so far={}
Unifying symbol X with li36 vars=set([X, E]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([E]), so far={X: li36}
Unifying symbol E with () vars=set([E]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...searchDone, now 80) short=3, {18}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), X: li38}, {{18}:: li39 rdf:type NeedsEval}), ({E: (), X: li31}, {{18}:: li40 rdf:type NeedsEval}), ({E: (), X: li36}, {{18}:: li41 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li38})
new binding: E -> ()
new binding: X -> li38
QUERY MATCH COMPLETE with bindings: {X: li38, E: ()}
Concluding tentatively...{X: li38, E: ()}
@@ Duplicate result: {X: li38, E: ()}
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li31})
new binding: E -> ()
new binding: X -> li31
QUERY MATCH COMPLETE with bindings: {X: li31, E: ()}
Concluding tentatively...{X: li31, E: ()}
Not duplicate: {X: li31, E: ()}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY E->() X->li31 {li2 rdf:type NeedsFindBinding}->{18}
Substition of variables {X: li31, E: (), {li2 rdf:type NeedsFindBinding}: {18}} in list li2
...yields NEW li40 = [[lambda, [x], x], []]
SubstituteEquals list li40 with {}
Add statement (size before 133, 18 statements) to {18}:
{li40 rdf:type NeedsFindBinding}
Added 1, nominal size of store changed from 133 to 134.
Nested query returns 1 fo {E: (), X: li31}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li36})
new binding: E -> ()
new binding: X -> li36
QUERY MATCH COMPLETE with bindings: {X: li36, E: ()}
Concluding tentatively...{X: li36, E: ()}
Not duplicate: {X: li36, E: ()}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY E->() X->li36 {li2 rdf:type NeedsFindBinding}->{19}
Substition of variables {X: li36, E: (), {li2 rdf:type NeedsFindBinding}: {19}} in list li2
...yields NEW li41 = [[lambda, [y], [y, y]], []]
SubstituteEquals list li41 with {}
Add statement (size before 134, 19 statements) to {19}:
{li41 rdf:type NeedsFindBinding}
Added 1, nominal size of store changed from 134 to 135.
Nested query returns 1 fo {E: (), X: li36}
Item state 80, returning total 2
Rule try generated 2 new statements
Rule R4 gave 2. Affects:[R1, R2*].
...rescheduling R1
...rescheduling R2*
Trying rule R5 ===================
{20} :: li2 rdf:type NeedsEval.
{20} :: li2 binds R.
Query: created with 2 terms. (justone=0, wc={20})
{20} :: li2 rdf:type NeedsEval.
{20} :: li2 binds R.
Smart in: [{20}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsEval needs to run: set([])
setup: 45) short=3, {20}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
binds needs to run: set([])
li2 needs to run: set([E, X])
R needs to run: set([R])
...searchDone, now 80) short=0, {20}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
setup: 80) short=0, {20}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
match: abandoned, no way for 80) short=0, {20}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
Rule try generated 0 new statements
Rule R5 gave 0. Affects:[R8].
Trying rule R6 ===================
{20} :: li17 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={20})
{20} :: li17 rdf:type NeedsEval.
Smart in: [{20}]
rdf:type needs to run: set([])
li17 needs to run: set([X, Y, F, E])
NeedsEval needs to run: set([])
setup: 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(F,X,E,Y) ExQuVars:()
Searching (S=45) 3 for 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li39 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with li31 vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li40 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[lambda, [x], x], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [lambda, [x], x] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with lambda vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li41 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[lambda, [y], [y, y]], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [lambda, [y], [y, y]] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with lambda vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=3, {20}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R6 gave 0. Affects:[R8].
Trying rule R7* ===================
{20} :: li18 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={20})
{20} :: li18 rdf:type NeedsEval.
Smart in: [{20}]
rdf:type needs to run: set([])
li18 needs to run: set([B, A, E])
NeedsEval needs to run: set([])
setup: 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(E,A,B) ExQuVars:()
Searching (S=45) 3 for 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li39 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([E, A, B]), so far={}
Unifying symbol A with li31 vars=set([E, A, B]), so far={}
Unifying term MATCHED A to li31
Unifying list [B] with [[lambda, [y], [y, y]]] vars=set([E, B]), so far={A: li31}
Unifying symbol B with li36 vars=set([E, B]), so far={A: li31}
Unifying term MATCHED B to li36
Unifying list [E] with [[]] vars=set([E]), so far={B: li36, A: li31}
Unifying symbol E with () vars=set([E]), so far={B: li36, A: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({A: li31, E: (), B: li36}, None)]
nb1 = {A: li31, E: (), B: li36}
nb = {}
...checking {{20}:: li40 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[lambda, [x], x], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [lambda, [x], x] vars=set([E, A, B]), so far={}
Unifying symbol A with lambda vars=set([E, A, B]), so far={}
Unifying term MATCHED A to lambda
Unifying list [B] with [[x], x] vars=set([E, B]), so far={A: lambda}
Unifying symbol B with li29 vars=set([E, B]), so far={A: lambda}
Unifying term MATCHED B to li29
Searching deep 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li41 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[lambda, [y], [y, y]], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [lambda, [y], [y, y]] vars=set([E, A, B]), so far={}
Unifying symbol A with lambda vars=set([E, A, B]), so far={}
Unifying term MATCHED A to lambda
Unifying list [B] with [[y], [y, y]] vars=set([E, B]), so far={A: lambda}
Unifying symbol B with li32 vars=set([E, B]), so far={A: lambda}
Unifying term MATCHED B to li32
Searching deep 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), A: li31, B: li36}, {{20}:: li39 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), A: li31, B: li36})
new binding: E -> ()
new binding: A -> li31
new binding: B -> li36
QUERY MATCH COMPLETE with bindings: {A: li31, E: (), B: li36}
Concluding tentatively...{A: li31, E: (), B: li36}
@@ Duplicate result: {A: li31, E: (), B: li36}
Nested query returns 0 fo {E: (), A: li31, B: li36}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R7* gave 0. Affects:[R3, R4, R5, R6, R7*, R8].
Trying rule R8 ===================
{20} :: li18 rdf:type NeedsEval.
{20} :: li19 eval F.
{20} :: li20 eval X.
Query: created with 3 terms. (justone=0, wc={20})
{20} :: li18 rdf:type NeedsEval.
{20} :: li19 eval F.
{20} :: li20 eval X.
Smart in: [{20}]
rdf:type needs to run: set([])
li18 needs to run: set([B, A, E])
NeedsEval needs to run: set([])
setup: 45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
eval needs to run: set([])
li19 needs to run: set([E, A])
F needs to run: set([F])
setup: 45) short=2, {20}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
eval needs to run: set([])
li20 needs to run: set([E, B])
X needs to run: set([X])
setup: 45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {20}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {20}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {20}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
Looking at 45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
...with vars(F,X) ExQuVars:(E,A,B)
Searching (S=45) 2 for 45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
...checking {{20}:: li40 eval li45}
Unifying list [B, E] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying symbol B with li31 vars=set([F, X]), so far={}
Unifying term MATCHED B to li31
Unifying list [E] with [[]] vars=set([X, F]), so far={B: li31}
Unifying symbol E with () vars=set([X, F]), so far={B: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?. result binding [({B: li31, E: ()}, None)]
nb1 = {B: li31, E: ()}
nb = {}
nb1 = {X: li45}
nb = {E: (), B: li31}
...checking {{20}:: li41 eval li48}
Unifying list [B, E] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying symbol B with li36 vars=set([F, X]), so far={}
Unifying term MATCHED B to li36
Unifying list [E] with [[]] vars=set([X, F]), so far={B: li36}
Unifying symbol E with () vars=set([X, F]), so far={B: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?. result binding [({B: li36, E: ()}, None)]
nb1 = {B: li36, E: ()}
nb = {}
nb1 = {X: li48}
nb = {E: (), B: li36}
...searchDone, now 80) short=2, {20}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
nbs=[({E: (), B: li31, X: li45}, {{20}:: li40 eval li45}), ({E: (), B: li36, X: li48}, {{20}:: li41 eval li48})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), B: li31, X: li45})
45) short=3, {20}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {20}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?.
new binding: E -> ()
new binding: B -> li31
new binding: X -> li45
binding 45) short=3, {20}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]). with {E: (), B: li31, X: li45}
Substition of variables {E: (), B: li31, X: li45} in list li5
...yields NEW li50 = [A, [lambda, [x], x]]
Substition of variables {E: (), B: li31, X: li45} in list li18
...yields NEW li51 = [[A, [lambda, [x], x]], []]
...bound becomes 45) short=3, {20}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
binding 45) short=2, {20}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?. with {E: (), B: li31, X: li45}
Substition of variables {E: (), B: li31, X: li45} in list li19
...yields NEW li52 = [A, []]
...bound becomes 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
query iterating with 2 terms, 1 bindings: X->li45 ; 3 new bindings: E->() B->li31 X->li45 .
45) short=3, {20}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
Looking at 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...with vars(F) ExQuVars:(A)
Searching (S=45) 2 for 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...checking {{20}:: li40 eval li45}
Unifying list [A, []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying symbol A with li31 vars=set([F, X]), so far={}
Unifying term MATCHED A to li31
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li31}
Searching deep 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li31}, None)]
nb1 = {A: li31}
nb = {}
nb1 = {F: li45}
nb = {A: li31}
...checking {{20}:: li41 eval li48}
Unifying list [A, []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying symbol A with li36 vars=set([F, X]), so far={}
Unifying term MATCHED A to li36
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li36}
Searching deep 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li36}, None)]
nb1 = {A: li36}
nb = {}
nb1 = {F: li48}
nb = {A: li36}
...searchDone, now 80) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
nbs=[({F: li45, A: li31}, {{20}:: li40 eval li45}), ({F: li48, A: li36}, {{20}:: li41 eval li48})]
QUERY2: called 1 terms, 1 bindings {X: li45}, (new: {F: li45, A: li31})
45) short=3, {20}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li45
new binding: A -> li31
binding 45) short=3, {20}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li45, A: li31}
Substition of variables {F: li45, A: li31} in list li50
...yields NEW li53 = [[lambda, [x], x], [lambda, [x], x]]
Substition of variables {F: li45, A: li31} in list li51
...yields NEW li54 = [[[lambda, [x], x], [lambda, [x], x]], []]
...bound becomes 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li45 X->li45 ; 2 new bindings: F->li45 A->li31 .
45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 3 for 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x]] with [[lambda, [y], [y, y]]] vars=set([X, F]), so far={}
Unifying list [lambda, [x], x] with [lambda, [y], [y, y]] vars=set([X, F]), so far={}
Unifying symbol lambda with lambda vars=set([X, F]), so far={}
Unifying list [[x], x] with [[y], [y, y]] vars=set([F, X]), so far={}
Unifying list [x] with [y] vars=set([F, X]), so far={}
Unifying symbol x with y vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=3, {20}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {F: li45, A: li31}
QUERY2: called 1 terms, 1 bindings {X: li45}, (new: {F: li48, A: li36})
45) short=3, {20}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li48
new binding: A -> li36
binding 45) short=3, {20}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li48, A: li36}
Substition of variables {F: li48, A: li36} in list li50
...yields NEW li55 = [[lambda, [y], [y, y]], [lambda, [x], x]]
Substition of variables {F: li48, A: li36} in list li51
...yields NEW li56 = [[[lambda, [y], [y, y]], [lambda, [x], x]], []]
...bound becomes 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li48 X->li45 ; 2 new bindings: F->li48 A->li36 .
45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 3 for 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying symbol lambda with lambda vars=set([F, X]), so far={}
Unifying list [[y], [y, y]] with [[x], x] vars=set([X, F]), so far={}
Unifying list [y] with [x] vars=set([X, F]), so far={}
Unifying symbol y with x vars=set([X, F]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=3, {20}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {F: li48, A: li36}
Item state 80, returning total 0
Nested query returns 0 fo {E: (), B: li31, X: li45}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), B: li36, X: li48})
45) short=3, {20}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {20}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?.
new binding: E -> ()
new binding: B -> li36
new binding: X -> li48
binding 45) short=3, {20}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]). with {E: (), B: li36, X: li48}
Substition of variables {E: (), B: li36, X: li48} in list li5
...yields NEW li57 = [A, [lambda, [y], [y, y]]]
Substition of variables {E: (), B: li36, X: li48} in list li18
...yields NEW li58 = [[A, [lambda, [y], [y, y]]], []]
...bound becomes 45) short=3, {20}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
binding 45) short=2, {20}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?. with {E: (), B: li36, X: li48}
Substition of variables {E: (), B: li36, X: li48} in list li19
...yields NEW li52 = [A, []]
...bound becomes 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
query iterating with 2 terms, 1 bindings: X->li48 ; 3 new bindings: E->() B->li36 X->li48 .
45) short=3, {20}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
Looking at 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...with vars(F) ExQuVars:(A)
Searching (S=45) 2 for 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...checking {{20}:: li40 eval li45}
Unifying list [A, []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying symbol A with li31 vars=set([F, X]), so far={}
Unifying term MATCHED A to li31
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li31}
Searching deep 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li31}, None)]
nb1 = {A: li31}
nb = {}
nb1 = {F: li45}
nb = {A: li31}
...checking {{20}:: li41 eval li48}
Unifying list [A, []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying symbol A with li36 vars=set([F, X]), so far={}
Unifying term MATCHED A to li36
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li36}
Searching deep 45) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li36}, None)]
nb1 = {A: li36}
nb = {}
nb1 = {F: li48}
nb = {A: li36}
...searchDone, now 80) short=2, {20}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
nbs=[({F: li45, A: li31}, {{20}:: li40 eval li45}), ({F: li48, A: li36}, {{20}:: li41 eval li48})]
QUERY2: called 1 terms, 1 bindings {X: li48}, (new: {F: li45, A: li31})
45) short=3, {20}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li45
new binding: A -> li31
binding 45) short=3, {20}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li45, A: li31}
Substition of variables {F: li45, A: li31} in list li57
...yields NEW li38 = [[lambda, [x], x], [lambda, [y], [y, y]]]
Substition of variables {F: li45, A: li31} in list li58
...yields NEW li39 = [[[lambda, [x], x], [lambda, [y], [y, y]]], []]
...bound becomes 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li45 X->li48 ; 2 new bindings: F->li45 A->li31 .
45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 3 for 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding [({}, None)]
nb1 = {}
nb = {}
...checking {{20}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [y], [y, y]]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{20}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [y], [y, y]]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=3, {20}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({}, {{20}:: li39 rdf:type NeedsEval})]
QUERY2: called 0 terms, 2 bindings {X: li48, F: li45}, (new: {})
QUERY MATCH COMPLETE with bindings: {X: li48, F: li45}
Concluding tentatively...{X: li48, F: li45}
Not duplicate: {X: li48, F: li45}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY F->li45 {li21 rdf:type NeedsApply}->{20} X->li48
Substition of variables {{li21 rdf:type NeedsApply}: {20}, F: li45, X: li48} in list li21
...yields NEW li60 = [[function, x, x, []], [function, y, [y, y], []]]
SubstituteEquals list li60 with {}
Add statement (size before 135, 20 statements) to {20}:
{li60 rdf:type NeedsApply}
Added 1, nominal size of store changed from 135 to 136.
Nested query returns 1 fo {}
Item state 80, returning total 1
Nested query returns 1 fo {F: li45, A: li31}
QUERY2: called 1 terms, 1 bindings {X: li48}, (new: {F: li48, A: li36})
45) short=3, {21}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li48
new binding: A -> li36
binding 45) short=3, {21}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li48, A: li36}
Substition of variables {F: li48, A: li36} in list li57
...yields NEW li61 = [[lambda, [y], [y, y]], [lambda, [y], [y, y]]]
Substition of variables {F: li48, A: li36} in list li58
...yields NEW li62 = [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []]
...bound becomes 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li48 X->li48 ; 2 new bindings: F->li48 A->li36 .
45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 3 for 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{21}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying symbol lambda with lambda vars=set([F, X]), so far={}
Unifying list [[y], [y, y]] with [[x], x] vars=set([X, F]), so far={}
Unifying list [y] with [x] vars=set([X, F]), so far={}
Unifying symbol y with x vars=set([X, F]), so far={}
Searching deep 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{21}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{21}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=3, {21}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {F: li48, A: li36}
Item state 80, returning total 1
Nested query returns 1 fo {E: (), B: li36, X: li48}
Item state 80, returning total 1
Rule try generated 1 new statements
Rule R8 gave 1. Affects:[R9].
...rescheduling R9
Trying rule R1 ===================
{21} :: li2 rdf:type NeedsFindBinding.
{21} :: E rdf:first li4.
{21} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={21})
{21} :: li2 rdf:type NeedsFindBinding.
{21} :: E rdf:first li4.
{21} :: E rdf:rest R.
Smart in: [{21}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li4 needs to run: set([B, X])
setup: 50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...searchDone, now 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
Looking at 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,E,B) ExQuVars:(R)
Searching (S=45) 3 for 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{21}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li38 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li38}
Unifying symbol E with () vars=set([E, B]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{21}:: li40 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li31 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li31}
Unifying symbol E with () vars=set([E, B]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{21}:: li41 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li36 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li36}
Unifying symbol E with () vars=set([E, B]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...searchDone, now 80) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{21}:: li39 rdf:type NeedsFindBinding}), ({E: (), X: li31}, {{21}:: li40 rdf:type NeedsFindBinding}), ({E: (), X: li36}, {{21}:: li41 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li38}
Substition of variables {E: (), X: li38} in list li4
...yields NEW li42 = [[[lambda, [x], x], [lambda, [y], [y, y]]], B]
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
query iterating with 2 terms, 2 bindings: X->li38 E->() ; 2 new bindings: E->() X->li38 .
65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
Looking at 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li31})
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li31
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li31}
Substition of variables {E: (), X: li31} in list li4
...yields NEW li63 = [[lambda, [x], x], B]
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
query iterating with 2 terms, 2 bindings: X->li31 E->() ; 2 new bindings: E->() X->li31 .
65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
Looking at 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li31}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li36})
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li36
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li36}
Substition of variables {E: (), X: li36} in list li4
...yields NEW li64 = [[lambda, [y], [y, y]], B]
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
query iterating with 2 terms, 2 bindings: X->li36 E->() ; 2 new bindings: E->() X->li36 .
65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
Looking at 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li36}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R1 gave 0. Affects:[R5].
Trying rule R2* ===================
{21} :: li2 rdf:type NeedsFindBinding.
{21} :: E rdf:first li5.
{21} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={21})
{21} :: li2 rdf:type NeedsFindBinding.
{21} :: E rdf:first li5.
{21} :: E rdf:rest R.
Smart in: [{21}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li5 needs to run: set([B, A])
setup: 50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=50) 0 for 50) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=50) 0 for 50) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
...searchDone, now 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
Looking at 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=45) 3 for 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{21}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, R]), so far={}
Unifying symbol X with li38 vars=set([X, R]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([R]), so far={X: li38}
Unifying symbol E with () vars=set([R]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{21}:: li40 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, R]), so far={}
Unifying symbol X with li31 vars=set([X, R]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([R]), so far={X: li31}
Unifying symbol E with () vars=set([R]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{21}:: li41 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, R]), so far={}
Unifying symbol X with li36 vars=set([X, R]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([R]), so far={X: li36}
Unifying symbol E with () vars=set([R]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...searchDone, now 80) short=3, {21}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{21}:: li39 rdf:type NeedsFindBinding}), ({E: (), X: li31}, {{21}:: li40 rdf:type NeedsFindBinding}), ({E: (), X: li36}, {{21}:: li41 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li38 ; 2 new bindings: E->() X->li38 .
65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li31})
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li31
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li31 ; 2 new bindings: E->() X->li31 .
65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li31}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li36})
30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li36
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {21}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li36 ; 2 new bindings: E->() X->li36 .
65) short=7730, {21}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {21}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li36}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R2* gave 0. Affects:[R1, R2*].
Trying rule R9 ===================
{21} :: li23 rdf:type NeedsApply.
Query: created with 1 terms. (justone=0, wc={21})
{21} :: li23 rdf:type NeedsApply.
Smart in: [{21}]
rdf:type needs to run: set([])
li23 needs to run: set([X, Y, A, E])
NeedsApply needs to run: set([])
setup: 45) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
Looking at 45) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
...with vars(A,X,Y,E) ExQuVars:()
Searching (S=45) 1 for 45) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
...checking {{21}:: li60 rdf:type NeedsApply}
Unifying list [[function, X, Y, E], A] with [[function, x, x, []], [function, y, [y, y], []]] vars=set([A, X, Y, E]), so far={}
Unifying list [function, X, Y, E] with [function, x, x, []] vars=set([A, X, Y, E]), so far={}
Unifying symbol function with function vars=set([A, X, Y, E]), so far={}
Unifying list [X, Y, E] with [x, x, []] vars=set([X, A, Y, E]), so far={}
Unifying symbol X with x vars=set([X, A, Y, E]), so far={}
Unifying term MATCHED X to x
Unifying list [Y, E] with [x, []] vars=set([A, Y, E]), so far={X: x}
Unifying symbol Y with x vars=set([A, Y, E]), so far={X: x}
Unifying term MATCHED Y to x
Unifying list [E] with [[]] vars=set([A, E]), so far={Y: x, X: x}
Unifying symbol E with () vars=set([A, E]), so far={Y: x, X: x}
Unifying term MATCHED E to ()
Unifying list [A] with [[function, y, [y, y], []]] vars=set([A]), so far={E: (), Y: x, X: x}
Unifying symbol A with li48 vars=set([A]), so far={E: (), Y: x, X: x}
Unifying term MATCHED A to li48
Searching deep 45) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]). result binding [({Y: x, A: li48, X: x, E: ()}, None)]
nb1 = {Y: x, A: li48, X: x, E: ()}
nb = {}
...searchDone, now 80) short=1, {21}(et([]) :: li23(et([X, Y, A, E])? rdf:type(et([]) NeedsApply(et([]).
nbs=[({A: li48, Y: x, X: x, E: ()}, {{21}:: li60 rdf:type NeedsApply})]
QUERY2: called 0 terms, 0 bindings {}, (new: {A: li48, Y: x, X: x, E: ()})
new binding: A -> li48
new binding: Y -> x
new binding: X -> x
new binding: E -> ()
QUERY MATCH COMPLETE with bindings: {Y: x, A: li48, X: x, E: ()}
Concluding tentatively...{Y: x, A: li48, X: x, E: ()}
Not duplicate: {Y: x, A: li48, X: x, E: ()}
Variables regenerated: universal set([]) existential: set([_g_L89C6]),exi _g_L89C6 -> _g26
Concluding DEFINITELY X->x Y->x {3}->{21} A->li48 E->() _g_L89C6->_g26
Declare existential: _g26
Substition of variables {{3}: {21}, A: li48, E: (), Y: x, X: x, _g_L89C6: _g26} in list li24
...yields NEW li65 = [x, [function, y, [y, y], []]]
SubstituteEquals list li65 with {}
Add statement (size before 136, 21 statements) to {21}:
{_g26 rdf:first li65}
Add statement (size before 137, 22 statements) to {22}:
{_g26 rdf:rest ()}
removing {{22}:: _g26 rdf:first li65}
New list was _g26, now li66 = [[x, [function, y, [y, y], []]]]
...New list newBindings {_g26: li66}
SubstituteEquals list li38 with {_g26: li66}
SubstituteEquals list li39 with {_g26: li66}
SubstituteEquals list li39 with {_g26: li66}
SubstituteEquals list li40 with {_g26: li66}
SubstituteEquals list li41 with {_g26: li66}
SubstituteEquals list li40 with {_g26: li66}
SubstituteEquals list li45 with {_g26: li66}
SubstituteEquals list li41 with {_g26: li66}
SubstituteEquals list li48 with {_g26: li66}
SubstituteEquals list li40 with {_g26: li66}
SubstituteEquals list li41 with {_g26: li66}
SubstituteEquals list li60 with {_g26: li66}
Substitions {} generated {}
Substition of variables {{3}: {21}, A: li48, E: (), Y: x, X: x, _g_L89C6: _g26} in list li26
...yields NEW li68 = [x, _g26]
SubstituteEquals list li68 with {_g26: li66}
SubstitueEquals list CHANGED li68 -> li70
Add statement (size before 137, 21 statements) to {21}:
{li70 rdf:type NeedsEval}
SubstituteEquals list li38 with {li68: li70}
SubstituteEquals list li39 with {li68: li70}
SubstituteEquals list li39 with {li68: li70}
SubstituteEquals list li40 with {li68: li70}
SubstituteEquals list li41 with {li68: li70}
SubstituteEquals list li40 with {li68: li70}
SubstituteEquals list li45 with {li68: li70}
SubstituteEquals list li41 with {li68: li70}
SubstituteEquals list li48 with {li68: li70}
SubstituteEquals list li40 with {li68: li70}
SubstituteEquals list li41 with {li68: li70}
SubstituteEquals list li60 with {li68: li70}
Substitions {} generated {}
Added 3, nominal size of store changed from 136 to 138.
Nested query returns 3 fo {A: li48, Y: x, X: x, E: ()}
Item state 80, returning total 3
Rule try generated 3 new statements
Rule R9 gave 3. Affects:[R1, R2*, R3, R4, R5, R6, R7*, R8].
...rescheduling R1
...rescheduling R2*
...rescheduling R3
...rescheduling R4
...rescheduling R5
...rescheduling R6
...rescheduling R7*
...rescheduling R8
Trying rule R1 ===================
{22} :: li2 rdf:type NeedsFindBinding.
{22} :: E rdf:first li4.
{22} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={22})
{22} :: li2 rdf:type NeedsFindBinding.
{22} :: E rdf:first li4.
{22} :: E rdf:rest R.
Smart in: [{22}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li4 needs to run: set([B, X])
setup: 50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...searchDone, now 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
Looking at 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,E,B) ExQuVars:(R)
Searching (S=45) 3 for 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{22}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li38 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li38}
Unifying symbol E with () vars=set([E, B]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{22}:: li40 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li31 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li31}
Unifying symbol E with () vars=set([E, B]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{22}:: li41 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li36 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li36}
Unifying symbol E with () vars=set([E, B]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...searchDone, now 80) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{22}:: li39 rdf:type NeedsFindBinding}), ({E: (), X: li31}, {{22}:: li40 rdf:type NeedsFindBinding}), ({E: (), X: li36}, {{22}:: li41 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li38}
Substition of variables {E: (), X: li38} in list li4
...yields NEW li42 = [[[lambda, [x], x], [lambda, [y], [y, y]]], B]
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
query iterating with 2 terms, 2 bindings: X->li38 E->() ; 2 new bindings: E->() X->li38 .
65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
Looking at 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li31})
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li31
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li31}
Substition of variables {E: (), X: li31} in list li4
...yields NEW li63 = [[lambda, [x], x], B]
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
query iterating with 2 terms, 2 bindings: X->li31 E->() ; 2 new bindings: E->() X->li31 .
65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
Looking at 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li31}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li36})
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li36
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li36}
Substition of variables {E: (), X: li36} in list li4
...yields NEW li64 = [[lambda, [y], [y, y]], B]
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
query iterating with 2 terms, 2 bindings: X->li36 E->() ; 2 new bindings: E->() X->li36 .
65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
Looking at 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li36}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R1 gave 0. Affects:[R5].
Trying rule R2* ===================
{22} :: li2 rdf:type NeedsFindBinding.
{22} :: E rdf:first li5.
{22} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={22})
{22} :: li2 rdf:type NeedsFindBinding.
{22} :: E rdf:first li5.
{22} :: E rdf:rest R.
Smart in: [{22}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li5 needs to run: set([B, A])
setup: 50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=50) 0 for 50) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=50) 0 for 50) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
...searchDone, now 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([B, A])?.
Looking at 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,R) ExQuVars:(E,A,B)
Searching (S=45) 3 for 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{22}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, R]), so far={}
Unifying symbol X with li38 vars=set([X, R]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([R]), so far={X: li38}
Unifying symbol E with () vars=set([R]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{22}:: li40 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, R]), so far={}
Unifying symbol X with li31 vars=set([X, R]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([R]), so far={X: li31}
Unifying symbol E with () vars=set([R]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{22}:: li41 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, R]), so far={}
Unifying symbol X with li36 vars=set([X, R]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([R]), so far={X: li36}
Unifying symbol E with () vars=set([R]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...searchDone, now 80) short=3, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{22}:: li39 rdf:type NeedsFindBinding}), ({E: (), X: li31}, {{22}:: li40 rdf:type NeedsFindBinding}), ({E: (), X: li36}, {{22}:: li41 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li38 ; 2 new bindings: E->() X->li38 .
65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li31})
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li31
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li31 ; 2 new bindings: E->() X->li31 .
65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li31}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li36})
30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?.
new binding: E -> ()
new binding: X -> li36
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {22}(et([]) :: E(et([E])? rdf:first(et([]) li5(et([A, B])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
query iterating with 2 terms, 1 bindings: X->li36 ; 2 new bindings: E->() X->li36 .
65) short=7730, {22}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
Looking at 65) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
...with vars(R) ExQuVars:(A,B)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {22}(et([]) :: ()(et([]) rdf:first(et([]) li5(et([A, B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li36}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R2* gave 0. Affects:[R1, R2*].
Trying rule R3 ===================
{22} :: li12 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={22})
{22} :: li12 rdf:type NeedsEval.
Smart in: [{22}]
rdf:type needs to run: set([])
li12 needs to run: set([Y, X, E])
NeedsEval needs to run: set([])
setup: 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(X,E,Y) ExQuVars:()
Searching (S=45) 4 for 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{22}:: li39 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with li31 vars=set([X, E, Y]), so far={}
Searching deep 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{22}:: li40 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[lambda, [x], x], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [lambda, [x], x] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with lambda vars=set([X, E, Y]), so far={}
Unifying list [[X], Y] with [[x], x] vars=set([E, X, Y]), so far={}
Unifying list [X] with [x] vars=set([E, X, Y]), so far={}
Unifying symbol X with x vars=set([E, X, Y]), so far={}
Unifying term MATCHED X to x
Unifying list [Y] with [x] vars=set([E, Y]), so far={X: x}
Unifying symbol Y with x vars=set([E, Y]), so far={X: x}
Unifying term MATCHED Y to x
Unifying list [E] with [[]] vars=set([E]), so far={X: x, Y: x}
Unifying symbol E with () vars=set([E]), so far={X: x, Y: x}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({Y: x, E: (), X: x}, None)]
nb1 = {Y: x, E: (), X: x}
nb = {}
...checking {{22}:: li41 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [[lambda, [y], [y, y]], []] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with [lambda, [y], [y, y]] vars=set([X, E, Y]), so far={}
Unifying symbol lambda with lambda vars=set([X, E, Y]), so far={}
Unifying list [[X], Y] with [[y], [y, y]] vars=set([E, X, Y]), so far={}
Unifying list [X] with [y] vars=set([E, X, Y]), so far={}
Unifying symbol X with y vars=set([E, X, Y]), so far={}
Unifying term MATCHED X to y
Unifying list [Y] with [[y, y]] vars=set([E, Y]), so far={X: y}
Unifying symbol Y with li33 vars=set([E, Y]), so far={X: y}
Unifying term MATCHED Y to li33
Unifying list [E] with [[]] vars=set([E]), so far={X: y, Y: li33}
Unifying symbol E with () vars=set([E]), so far={X: y, Y: li33}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({Y: li33, E: (), X: y}, None)]
nb1 = {Y: li33, E: (), X: y}
nb = {}
...checking {{22}:: li70 rdf:type NeedsEval}
Unifying list [[lambda, [X], Y], E] with [x, [[x, [function, y, [y, y], []]]]] vars=set([X, E, Y]), so far={}
Unifying list [lambda, [X], Y] with x vars=set([X, E, Y]), so far={}
Searching deep 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {22}(et([]) :: li12(et([Y, X, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), Y: x, X: x}, {{22}:: li40 rdf:type NeedsEval}), ({E: (), Y: li33, X: y}, {{22}:: li41 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), Y: x, X: x})
new binding: E -> ()
new binding: Y -> x
new binding: X -> x
QUERY MATCH COMPLETE with bindings: {Y: x, E: (), X: x}
Concluding tentatively...{Y: x, E: (), X: x}
@@ Duplicate result: {Y: x, E: (), X: x}
Nested query returns 0 fo {E: (), Y: x, X: x}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), Y: li33, X: y})
new binding: E -> ()
new binding: Y -> li33
new binding: X -> y
QUERY MATCH COMPLETE with bindings: {Y: li33, E: (), X: y}
Concluding tentatively...{Y: li33, E: (), X: y}
@@ Duplicate result: {Y: li33, E: (), X: y}
Nested query returns 0 fo {E: (), Y: li33, X: y}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R3 gave 0. Affects:[R8].
Trying rule R4 ===================
{22} :: li2 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={22})
{22} :: li2 rdf:type NeedsEval.
Smart in: [{22}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsEval needs to run: set([])
setup: 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
...with vars(X,E) ExQuVars:()
Searching (S=45) 4 for 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
...checking {{22}:: li39 rdf:type NeedsEval}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E]), so far={}
Unifying symbol X with li38 vars=set([X, E]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E]), so far={X: li38}
Unifying symbol E with () vars=set([E]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{22}:: li40 rdf:type NeedsEval}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, E]), so far={}
Unifying symbol X with li31 vars=set([X, E]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([E]), so far={X: li31}
Unifying symbol E with () vars=set([E]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{22}:: li41 rdf:type NeedsEval}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, E]), so far={}
Unifying symbol X with li36 vars=set([X, E]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([E]), so far={X: li36}
Unifying symbol E with () vars=set([E]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...checking {{22}:: li70 rdf:type NeedsEval}
Unifying list [X, E] with [x, [[x, [function, y, [y, y], []]]]] vars=set([X, E]), so far={}
Unifying symbol X with x vars=set([X, E]), so far={}
Unifying term MATCHED X to x
Unifying list [E] with [[[x, [function, y, [y, y], []]]]] vars=set([E]), so far={X: x}
Unifying symbol E with li66 vars=set([E]), so far={X: x}
Unifying term MATCHED E to li66
Searching deep 45) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]). result binding [({X: x, E: li66}, None)]
nb1 = {X: x, E: li66}
nb = {}
...searchDone, now 80) short=4, {22}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), X: li38}, {{22}:: li39 rdf:type NeedsEval}), ({E: (), X: li31}, {{22}:: li40 rdf:type NeedsEval}), ({E: (), X: li36}, {{22}:: li41 rdf:type NeedsEval}), ({E: li66, X: x}, {{22}:: li70 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li38})
new binding: E -> ()
new binding: X -> li38
QUERY MATCH COMPLETE with bindings: {X: li38, E: ()}
Concluding tentatively...{X: li38, E: ()}
@@ Duplicate result: {X: li38, E: ()}
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li31})
new binding: E -> ()
new binding: X -> li31
QUERY MATCH COMPLETE with bindings: {X: li31, E: ()}
Concluding tentatively...{X: li31, E: ()}
@@ Duplicate result: {X: li31, E: ()}
Nested query returns 0 fo {E: (), X: li31}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), X: li36})
new binding: E -> ()
new binding: X -> li36
QUERY MATCH COMPLETE with bindings: {X: li36, E: ()}
Concluding tentatively...{X: li36, E: ()}
@@ Duplicate result: {X: li36, E: ()}
Nested query returns 0 fo {E: (), X: li36}
QUERY2: called 0 terms, 0 bindings {}, (new: {E: li66, X: x})
new binding: E -> li66
new binding: X -> x
QUERY MATCH COMPLETE with bindings: {X: x, E: li66}
Concluding tentatively...{X: x, E: li66}
Not duplicate: {X: x, E: li66}
Variables regenerated: universal set([]) existential: set([])
Concluding DEFINITELY E->li66 X->x {li2 rdf:type NeedsFindBinding}->{22}
Substition of variables {X: x, E: li66, {li2 rdf:type NeedsFindBinding}: {22}} in list li2
...yields NEW li70 = [x, [[x, [function, y, [y, y], []]]]]
SubstituteEquals list li70 with {li68: li70, _g26: li66}
Add statement (size before 138, 22 statements) to {22}:
{li70 rdf:type NeedsFindBinding}
Added 1, nominal size of store changed from 138 to 139.
Nested query returns 1 fo {E: li66, X: x}
Item state 80, returning total 1
Rule try generated 1 new statements
Rule R4 gave 1. Affects:[R1, R2*].
...rescheduling R1
...rescheduling R2*
Trying rule R5 ===================
{23} :: li2 rdf:type NeedsEval.
{23} :: li2 binds R.
Query: created with 2 terms. (justone=0, wc={23})
{23} :: li2 rdf:type NeedsEval.
{23} :: li2 binds R.
Smart in: [{23}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsEval needs to run: set([])
setup: 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsEval(et([]).
binds needs to run: set([])
li2 needs to run: set([E, X])
R needs to run: set([R])
...searchDone, now 80) short=0, {23}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
setup: 80) short=0, {23}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
match: abandoned, no way for 80) short=0, {23}(et([]) :: li2(et([E, X])? binds(et([]) R(et([R])?.
Rule try generated 0 new statements
Rule R5 gave 0. Affects:[R8].
Trying rule R6 ===================
{23} :: li17 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={23})
{23} :: li17 rdf:type NeedsEval.
Smart in: [{23}]
rdf:type needs to run: set([])
li17 needs to run: set([X, Y, F, E])
NeedsEval needs to run: set([])
setup: 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(F,X,E,Y) ExQuVars:()
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li39 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with li31 vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li40 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[lambda, [x], x], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [lambda, [x], x] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with lambda vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li41 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [[lambda, [y], [y, y]], []] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with [lambda, [y], [y, y]] vars=set([F, X, E, Y]), so far={}
Unifying symbol function with lambda vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li70 rdf:type NeedsEval}
Unifying list [[function, X, Y, E], F] with [x, [[x, [function, y, [y, y], []]]]] vars=set([F, X, E, Y]), so far={}
Unifying list [function, X, Y, E] with x vars=set([F, X, E, Y]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {23}(et([]) :: li17(et([X, Y, F, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R6 gave 0. Affects:[R8].
Trying rule R7* ===================
{23} :: li18 rdf:type NeedsEval.
Query: created with 1 terms. (justone=0, wc={23})
{23} :: li18 rdf:type NeedsEval.
Smart in: [{23}]
rdf:type needs to run: set([])
li18 needs to run: set([B, A, E])
NeedsEval needs to run: set([])
setup: 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
QUERY2: called 1 terms, 0 bindings {}, (new: {})
45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...with vars(E,A,B) ExQuVars:()
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li39 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([E, A, B]), so far={}
Unifying symbol A with li31 vars=set([E, A, B]), so far={}
Unifying term MATCHED A to li31
Unifying list [B] with [[lambda, [y], [y, y]]] vars=set([E, B]), so far={A: li31}
Unifying symbol B with li36 vars=set([E, B]), so far={A: li31}
Unifying term MATCHED B to li36
Unifying list [E] with [[]] vars=set([E]), so far={B: li36, A: li31}
Unifying symbol E with () vars=set([E]), so far={B: li36, A: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding [({A: li31, E: (), B: li36}, None)]
nb1 = {A: li31, E: (), B: li36}
nb = {}
...checking {{23}:: li40 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[lambda, [x], x], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [lambda, [x], x] vars=set([E, A, B]), so far={}
Unifying symbol A with lambda vars=set([E, A, B]), so far={}
Unifying term MATCHED A to lambda
Unifying list [B] with [[x], x] vars=set([E, B]), so far={A: lambda}
Unifying symbol B with li29 vars=set([E, B]), so far={A: lambda}
Unifying term MATCHED B to li29
Searching deep 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li41 rdf:type NeedsEval}
Unifying list [[A, B], E] with [[lambda, [y], [y, y]], []] vars=set([E, A, B]), so far={}
Unifying list [A, B] with [lambda, [y], [y, y]] vars=set([E, A, B]), so far={}
Unifying symbol A with lambda vars=set([E, A, B]), so far={}
Unifying term MATCHED A to lambda
Unifying list [B] with [[y], [y, y]] vars=set([E, B]), so far={A: lambda}
Unifying symbol B with li32 vars=set([E, B]), so far={A: lambda}
Unifying term MATCHED B to li32
Searching deep 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li70 rdf:type NeedsEval}
Unifying list [[A, B], E] with [x, [[x, [function, y, [y, y], []]]]] vars=set([E, A, B]), so far={}
Unifying list [A, B] with x vars=set([E, A, B]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({E: (), A: li31, B: li36}, {{23}:: li39 rdf:type NeedsEval})]
QUERY2: called 0 terms, 0 bindings {}, (new: {E: (), A: li31, B: li36})
new binding: E -> ()
new binding: A -> li31
new binding: B -> li36
QUERY MATCH COMPLETE with bindings: {A: li31, E: (), B: li36}
Concluding tentatively...{A: li31, E: (), B: li36}
@@ Duplicate result: {A: li31, E: (), B: li36}
Nested query returns 0 fo {E: (), A: li31, B: li36}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R7* gave 0. Affects:[R3, R4, R5, R6, R7*, R8].
Trying rule R8 ===================
{23} :: li18 rdf:type NeedsEval.
{23} :: li19 eval F.
{23} :: li20 eval X.
Query: created with 3 terms. (justone=0, wc={23})
{23} :: li18 rdf:type NeedsEval.
{23} :: li19 eval F.
{23} :: li20 eval X.
Smart in: [{23}]
rdf:type needs to run: set([])
li18 needs to run: set([B, A, E])
NeedsEval needs to run: set([])
setup: 45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
eval needs to run: set([])
li19 needs to run: set([E, A])
F needs to run: set([F])
setup: 45) short=2, {23}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
eval needs to run: set([])
li20 needs to run: set([E, B])
X needs to run: set([X])
setup: 45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {23}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {23}(et([]) :: li18(et([B, A, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {23}(et([]) :: li19(et([E, A])? eval(et([]) F(et([F])?.
45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
Looking at 45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
...with vars(F,X) ExQuVars:(E,A,B)
Searching (S=45) 2 for 45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
...checking {{23}:: li40 eval li45}
Unifying list [B, E] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying symbol B with li31 vars=set([F, X]), so far={}
Unifying term MATCHED B to li31
Unifying list [E] with [[]] vars=set([X, F]), so far={B: li31}
Unifying symbol E with () vars=set([X, F]), so far={B: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?. result binding [({B: li31, E: ()}, None)]
nb1 = {B: li31, E: ()}
nb = {}
nb1 = {X: li45}
nb = {E: (), B: li31}
...checking {{23}:: li41 eval li48}
Unifying list [B, E] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying symbol B with li36 vars=set([F, X]), so far={}
Unifying term MATCHED B to li36
Unifying list [E] with [[]] vars=set([X, F]), so far={B: li36}
Unifying symbol E with () vars=set([X, F]), so far={B: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?. result binding [({B: li36, E: ()}, None)]
nb1 = {B: li36, E: ()}
nb = {}
nb1 = {X: li48}
nb = {E: (), B: li36}
...searchDone, now 80) short=2, {23}(et([]) :: li20(et([E, B])? eval(et([]) X(et([X])?.
nbs=[({E: (), B: li31, X: li45}, {{23}:: li40 eval li45}), ({E: (), B: li36, X: li48}, {{23}:: li41 eval li48})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), B: li31, X: li45})
45) short=4, {23}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {23}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?.
new binding: E -> ()
new binding: B -> li31
new binding: X -> li45
binding 45) short=4, {23}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]). with {E: (), B: li31, X: li45}
Substition of variables {E: (), B: li31, X: li45} in list li5
...yields NEW li50 = [A, [lambda, [x], x]]
Substition of variables {E: (), B: li31, X: li45} in list li18
...yields NEW li51 = [[A, [lambda, [x], x]], []]
...bound becomes 45) short=4, {23}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
binding 45) short=2, {23}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?. with {E: (), B: li31, X: li45}
Substition of variables {E: (), B: li31, X: li45} in list li19
...yields NEW li52 = [A, []]
...bound becomes 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
query iterating with 2 terms, 1 bindings: X->li45 ; 3 new bindings: E->() B->li31 X->li45 .
45) short=4, {23}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
Looking at 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...with vars(F) ExQuVars:(A)
Searching (S=45) 2 for 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...checking {{23}:: li40 eval li45}
Unifying list [A, []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying symbol A with li31 vars=set([F, X]), so far={}
Unifying term MATCHED A to li31
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li31}
Searching deep 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li31}, None)]
nb1 = {A: li31}
nb = {}
nb1 = {F: li45}
nb = {A: li31}
...checking {{23}:: li41 eval li48}
Unifying list [A, []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying symbol A with li36 vars=set([F, X]), so far={}
Unifying term MATCHED A to li36
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li36}
Searching deep 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li36}, None)]
nb1 = {A: li36}
nb = {}
nb1 = {F: li48}
nb = {A: li36}
...searchDone, now 80) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
nbs=[({F: li45, A: li31}, {{23}:: li40 eval li45}), ({F: li48, A: li36}, {{23}:: li41 eval li48})]
QUERY2: called 1 terms, 1 bindings {X: li45}, (new: {F: li45, A: li31})
45) short=4, {23}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li45
new binding: A -> li31
binding 45) short=4, {23}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li45, A: li31}
Substition of variables {F: li45, A: li31} in list li50
...yields NEW li53 = [[lambda, [x], x], [lambda, [x], x]]
Substition of variables {F: li45, A: li31} in list li51
...yields NEW li54 = [[[lambda, [x], x], [lambda, [x], x]], []]
...bound becomes 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li45 X->li45 ; 2 new bindings: F->li45 A->li31 .
45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x]] with [[lambda, [y], [y, y]]] vars=set([X, F]), so far={}
Unifying list [lambda, [x], x] with [lambda, [y], [y, y]] vars=set([X, F]), so far={}
Unifying symbol lambda with lambda vars=set([X, F]), so far={}
Unifying list [[x], x] with [[y], [y, y]] vars=set([F, X]), so far={}
Unifying list [x] with [y] vars=set([F, X]), so far={}
Unifying symbol x with y vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li70 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [x], x]], []] with [x, [[x, [function, y, [y, y], []]]]] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [x], x]] with x vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {23}(et([]) :: li54(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {F: li45, A: li31}
QUERY2: called 1 terms, 1 bindings {X: li45}, (new: {F: li48, A: li36})
45) short=4, {23}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li48
new binding: A -> li36
binding 45) short=4, {23}(et([]) :: li51(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li48, A: li36}
Substition of variables {F: li48, A: li36} in list li50
...yields NEW li55 = [[lambda, [y], [y, y]], [lambda, [x], x]]
Substition of variables {F: li48, A: li36} in list li51
...yields NEW li56 = [[[lambda, [y], [y, y]], [lambda, [x], x]], []]
...bound becomes 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li48 X->li45 ; 2 new bindings: F->li48 A->li36 .
45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying symbol lambda with lambda vars=set([F, X]), so far={}
Unifying list [[y], [y, y]] with [[x], x] vars=set([X, F]), so far={}
Unifying list [y] with [x] vars=set([X, F]), so far={}
Unifying symbol y with x vars=set([X, F]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li70 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [x], x]], []] with [x, [[x, [function, y, [y, y], []]]]] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [x], x]] with x vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {23}(et([]) :: li56(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {F: li48, A: li36}
Item state 80, returning total 0
Nested query returns 0 fo {E: (), B: li31, X: li45}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), B: li36, X: li48})
45) short=4, {23}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {23}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?.
new binding: E -> ()
new binding: B -> li36
new binding: X -> li48
binding 45) short=4, {23}(et([]) :: li18(et([A, B, E])? rdf:type(et([]) NeedsEval(et([]). with {E: (), B: li36, X: li48}
Substition of variables {E: (), B: li36, X: li48} in list li5
...yields NEW li57 = [A, [lambda, [y], [y, y]]]
Substition of variables {E: (), B: li36, X: li48} in list li18
...yields NEW li58 = [[A, [lambda, [y], [y, y]]], []]
...bound becomes 45) short=4, {23}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
binding 45) short=2, {23}(et([]) :: li19(et([A, E])? eval(et([]) F(et([F])?. with {E: (), B: li36, X: li48}
Substition of variables {E: (), B: li36, X: li48} in list li19
...yields NEW li52 = [A, []]
...bound becomes 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
query iterating with 2 terms, 1 bindings: X->li48 ; 3 new bindings: E->() B->li36 X->li48 .
45) short=4, {23}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
Looking at 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...with vars(F) ExQuVars:(A)
Searching (S=45) 2 for 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
...checking {{23}:: li40 eval li45}
Unifying list [A, []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying symbol A with li31 vars=set([F, X]), so far={}
Unifying term MATCHED A to li31
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li31}
Searching deep 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li31}, None)]
nb1 = {A: li31}
nb = {}
nb1 = {F: li45}
nb = {A: li31}
...checking {{23}:: li41 eval li48}
Unifying list [A, []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying symbol A with li36 vars=set([F, X]), so far={}
Unifying term MATCHED A to li36
Unifying list [[]] with [[]] vars=set([X, F]), so far={A: li36}
Searching deep 45) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?. result binding [({A: li36}, None)]
nb1 = {A: li36}
nb = {}
nb1 = {F: li48}
nb = {A: li36}
...searchDone, now 80) short=2, {23}(et([]) :: li52(et([A])? eval(et([]) F(et([F])?.
nbs=[({F: li45, A: li31}, {{23}:: li40 eval li45}), ({F: li48, A: li36}, {{23}:: li41 eval li48})]
QUERY2: called 1 terms, 1 bindings {X: li48}, (new: {F: li45, A: li31})
45) short=4, {23}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li45
new binding: A -> li31
binding 45) short=4, {23}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li45, A: li31}
Substition of variables {F: li45, A: li31} in list li57
...yields NEW li38 = [[lambda, [x], x], [lambda, [y], [y, y]]]
Substition of variables {F: li45, A: li31} in list li58
...yields NEW li39 = [[[lambda, [x], x], [lambda, [y], [y, y]]], []]
...bound becomes 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li45 X->li48 ; 2 new bindings: F->li45 A->li31 .
45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding [({}, None)]
nb1 = {}
nb = {}
...checking {{23}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [y], [y, y]]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [y], [y, y]]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [x], x] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li70 rdf:type NeedsEval}
Unifying list [[[lambda, [x], x], [lambda, [y], [y, y]]], []] with [x, [[x, [function, y, [y, y], []]]]] vars=set([F, X]), so far={}
Unifying list [[lambda, [x], x], [lambda, [y], [y, y]]] with x vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {23}(et([]) :: li39(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[({}, {{23}:: li39 rdf:type NeedsEval})]
QUERY2: called 0 terms, 2 bindings {X: li48, F: li45}, (new: {})
QUERY MATCH COMPLETE with bindings: {X: li48, F: li45}
Concluding tentatively...{X: li48, F: li45}
@@ Duplicate result: {X: li48, F: li45}
Nested query returns 0 fo {}
Item state 80, returning total 0
Nested query returns 0 fo {F: li45, A: li31}
QUERY2: called 1 terms, 1 bindings {X: li48}, (new: {F: li48, A: li36})
45) short=4, {23}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]).
new binding: F -> li48
new binding: A -> li36
binding 45) short=4, {23}(et([]) :: li58(et([A])? rdf:type(et([]) NeedsEval(et([]). with {F: li48, A: li36}
Substition of variables {F: li48, A: li36} in list li57
...yields NEW li61 = [[lambda, [y], [y, y]], [lambda, [y], [y, y]]]
Substition of variables {F: li48, A: li36} in list li58
...yields NEW li62 = [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []]
...bound becomes 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
query iterating with 1 terms, 2 bindings: F->li48 X->li48 ; 2 new bindings: F->li48 A->li36 .
45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
Looking at 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...with vars() ExQuVars:()
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li39 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with [[lambda, [x], x], [lambda, [y], [y, y]]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying symbol lambda with lambda vars=set([F, X]), so far={}
Unifying list [[y], [y, y]] with [[x], x] vars=set([X, F]), so far={}
Unifying list [y] with [x] vars=set([X, F]), so far={}
Unifying symbol y with x vars=set([X, F]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li40 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [[lambda, [x], x], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with [lambda, [x], x] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li41 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [[lambda, [y], [y, y]], []] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with [lambda, [y], [y, y]] vars=set([F, X]), so far={}
Unifying list [lambda, [y], [y, y]] with lambda vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...checking {{23}:: li70 rdf:type NeedsEval}
Unifying list [[[lambda, [y], [y, y]], [lambda, [y], [y, y]]], []] with [x, [[x, [function, y, [y, y], []]]]] vars=set([F, X]), so far={}
Unifying list [[lambda, [y], [y, y]], [lambda, [y], [y, y]]] with x vars=set([F, X]), so far={}
Searching deep 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]). result binding 0
......fail: 45) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
...searchDone, now 80) short=4, {23}(et([]) :: li62(et([])? rdf:type(et([]) NeedsEval(et([]).
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {F: li48, A: li36}
Item state 80, returning total 0
Nested query returns 0 fo {E: (), B: li36, X: li48}
Item state 80, returning total 0
Rule try generated 0 new statements
Rule R8 gave 0. Affects:[R9].
Trying rule R1 ===================
{23} :: li2 rdf:type NeedsFindBinding.
{23} :: E rdf:first li4.
{23} :: E rdf:rest R.
Query: created with 3 terms. (justone=0, wc={23})
{23} :: li2 rdf:type NeedsFindBinding.
{23} :: E rdf:first li4.
{23} :: E rdf:rest R.
Smart in: [{23}]
rdf:type needs to run: set([])
li2 needs to run: set([E, X])
NeedsFindBinding needs to run: set([])
setup: 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
rdf:first needs to run: set([])
E needs to run: set([E])
li4 needs to run: set([B, X])
setup: 50) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
rdf:rest needs to run: set([])
E needs to run: set([E])
R needs to run: set([R])
setup: 50) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
QUERY2: called 3 terms, 0 bindings {}, (new: {})
45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
50) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
...searchDone, now 30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
50) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
Looking at 50) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...with vars(X,E,B) ExQuVars:(R)
Searching (S=50) 0 for 50) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
...searchDone, now 30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
nbs=[]
Item state 30, returning total 0
query iterating with 3 terms, 0 bindings: ; 0 new bindings: .
45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([B, X])?.
Looking at 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...with vars(X,E,B) ExQuVars:(R)
Searching (S=45) 4 for 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
...checking {{23}:: li39 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[[lambda, [x], x], [lambda, [y], [y, y]]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li38 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li38
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li38}
Unifying symbol E with () vars=set([E, B]), so far={X: li38}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li38, E: ()}, None)]
nb1 = {X: li38, E: ()}
nb = {}
...checking {{23}:: li40 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [x], x], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li31 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li31
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li31}
Unifying symbol E with () vars=set([E, B]), so far={X: li31}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li31, E: ()}, None)]
nb1 = {X: li31, E: ()}
nb = {}
...checking {{23}:: li41 rdf:type NeedsFindBinding}
Unifying list [X, E] with [[lambda, [y], [y, y]], []] vars=set([X, E, B]), so far={}
Unifying symbol X with li36 vars=set([X, E, B]), so far={}
Unifying term MATCHED X to li36
Unifying list [E] with [[]] vars=set([E, B]), so far={X: li36}
Unifying symbol E with () vars=set([E, B]), so far={X: li36}
Unifying term MATCHED E to ()
Searching deep 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: li36, E: ()}, None)]
nb1 = {X: li36, E: ()}
nb = {}
...checking {{23}:: li70 rdf:type NeedsFindBinding}
Unifying list [X, E] with [x, [[x, [function, y, [y, y], []]]]] vars=set([X, E, B]), so far={}
Unifying symbol X with x vars=set([X, E, B]), so far={}
Unifying term MATCHED X to x
Unifying list [E] with [[[x, [function, y, [y, y], []]]]] vars=set([E, B]), so far={X: x}
Unifying symbol E with li66 vars=set([E, B]), so far={X: x}
Unifying term MATCHED E to li66
Searching deep 45) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]). result binding [({X: x, E: li66}, None)]
nb1 = {X: x, E: li66}
nb = {}
...searchDone, now 80) short=4, {23}(et([]) :: li2(et([E, X])? rdf:type(et([]) NeedsFindBinding(et([]).
nbs=[({E: (), X: li38}, {{23}:: li39 rdf:type NeedsFindBinding}), ({E: (), X: li31}, {{23}:: li40 rdf:type NeedsFindBinding}), ({E: (), X: li36}, {{23}:: li41 rdf:type NeedsFindBinding}), ({E: li66, X: x}, {{23}:: li70 rdf:type NeedsFindBinding})]
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li38})
30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li38
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li38}
...bound becomes 65) short=7730, {23}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li38}
Substition of variables {E: (), X: li38} in list li4
...yields NEW li42 = [[[lambda, [x], x], [lambda, [y], [y, y]]], B]
...bound becomes 65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
query iterating with 2 terms, 2 bindings: X->li38 E->() ; 2 new bindings: E->() X->li38 .
65) short=7730, {23}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
Looking at 65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li42(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li38}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li31})
30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li31
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li31}
...bound becomes 65) short=7730, {23}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li31}
Substition of variables {E: (), X: li31} in list li4
...yields NEW li63 = [[lambda, [x], x], B]
...bound becomes 65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
query iterating with 2 terms, 2 bindings: X->li31 E->() ; 2 new bindings: E->() X->li31 .
65) short=7730, {23}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
Looking at 65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li63(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li31}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: (), X: li36})
30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> ()
new binding: X -> li36
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: (), X: li36}
...bound becomes 65) short=7730, {23}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: (), X: li36}
Substition of variables {E: (), X: li36} in list li4
...yields NEW li64 = [[lambda, [y], [y, y]], B]
...bound becomes 65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
query iterating with 2 terms, 2 bindings: X->li36 E->() ; 2 new bindings: E->() X->li36 .
65) short=7730, {23}(et([]) :: ()(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
Looking at 65) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(())
Builtin could not give result 80) short=7730, {23}(et([]) :: ()(et([]) rdf:first(et([]) li64(et([B])?.
nbs=[]
Item state 80, returning total 0
Nested query returns 0 fo {E: (), X: li36}
QUERY2: called 2 terms, 0 bindings {}, (new: {E: li66, X: x})
30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?.
30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?.
new binding: E -> li66
new binding: X -> x
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:rest(et([]) R(et([R])?. with {E: li66, X: x}
...bound becomes 65) short=7730, {23}(et([]) :: li66(et([]) rdf:rest(et([]) R(et([R])?.
binding 30) short=0, {23}(et([]) :: E(et([E])? rdf:first(et([]) li4(et([X, B])?. with {E: li66, X: x}
Substition of variables {E: li66, X: x} in list li4
...yields NEW li71 = [x, B]
...bound becomes 65) short=7730, {23}(et([]) :: li66(et([]) rdf:first(et([]) li71(et([B])?.
query iterating with 2 terms, 2 bindings: X->x E->li66 ; 2 new bindings: E->li66 X->x .
65) short=7730, {23}(et([]) :: li66(et([]) rdf:rest(et([]) R(et([R])?.
65) short=7730, {23}(et([]) :: li66(et([]) rdf:first(et([]) li71(et([B])?.
Looking at 65) short=7730, {23}(et([]) :: li66(et([]) rdf:first(et([]) li71(et([B])?.
...with vars(B) ExQuVars:(R)
Builtin function call rdf:first(li66)
nbs=[({li71: li65}, None)]
QUERY2: called 1 terms, 2 bindings {E: li66, X: x}, (new: {li71: li65})
65) short=7730, {23}(et([]) :: li66(et([]) rdf:rest(et([]) R(et([R])?.
new binding: li71 -> li65
@@@ Not in existentials or variables but now bound: li71
#Processed by Id: cwm.py,v 1.167 2005/01/10 19:15:22 syosi Exp
# using base http://www.w3.org/2000/10/swap/test/turing/lambda.n3
Traceback (most recent call last):
File "/home/syosi/SWAP/cwm.py", line 652, in ?
doCommand()
File "/home/syosi/SWAP/cwm.py", line 563, in doCommand
think(workingContext, mode=option_flags["think"])
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 62, in think
return InferenceTask(knowledgeBase, ruleFormula, mode=mode, repeat=1).run()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 222, in run
return self.runSmart()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 210, in runSmart
total += cy.run()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 351, in run
found = rule.once()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 443, in once
total = query.resolve()
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 587, in resolve
return self.unify(self.queue, self.variables, self.existentials)
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 827, in unify
bindings.copy(), nb, evidence = evidence + [reason])
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 827, in unify
bindings.copy(), nb, evidence = evidence + [reason])
File "/home/syosi/cvs-trunk/WWW/2000/10/swap/query.py", line 715, in unify
existentials.remove(pair[0]) # Can't match anything anymore, need exact match
KeyError: li71
Received on Tuesday, 24 May 2005 03:40:39 UTC