- From: Jos De_Roo <jos.deroo@agfa.com>
- Date: Sun, 30 Mar 2003 21:41:44 +0200
- To: www-archive@w3.org
# Generated with http://www.agfa.com/w3c/euler/#R3389 on 2003-03-30 7:39:31
PM
# for query http://www.agfa.com/w3c/2002/02/thesis/booleW.q.n3
# given http://www.agfa.com/w3c/2002/02/thesis/booleW.a.n3
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <http://www.agfa.com/w3c/2002/02/thesis/boole#> .
{{?G = :g9. ?A = :a15. ?G :gnand1 ?A} log:implies {:g9 :gnand1 :a15} .
{?G = :g9. ?B = :a11. ?G :gnand2 ?B} log:implies {:g9 :gnand2 :a11} .
{?G = :g9. ?C = :cout. ?G :gnand3 ?C} log:implies {:g9 :gnand3 :cout} .
{{?G1 = :g5. ?G2 = :g8. ?G1 :nandnand1 ?G2} log:implies {:g5 :nandnand1
:g8} .
{?G1 = :g5. ?X = :a15. ?G1 :gnand3 ?X} log:implies {:g5 :gnand3 :a15} .
{?G2 = :g8. ?X = :a15. ?G2 :gnand1 ?X} log:implies {:g8 :gnand1 :a15} .
{{?G = :g5. ?A = :a14. ?G :gnand1 ?A} log:implies {:g5 :gnand1 :a14} .
{?G = :g5. ?B = :cin. ?G :gnand2 ?B} log:implies {:g5 :gnand2 :cin} .
{?G = :g5. ?C = :a15. ?G :gnand3 ?C} log:implies {:g5 :gnand3 :a15} .
{{?G1 = :g4. ?G2 = :g6. ?G1 :nandnand1 ?G2} log:implies {:g4
:nandnand1 :g6} .
{?G1 = :g4. ?X = :a14. ?G1 :gnand3 ?X} log:implies {:g4 :gnand3
:a14} .
{?G2 = :g6. ?X = :a14. ?G2 :gnand1 ?X} log:implies {:g6 :gnand1
:a14} .
{{?G = :g4. ?A = :a12. ?G :gnand1 ?A} log:implies {:g4 :gnand1
:a12} .
{?G = :g4. ?B = :a13. ?G :gnand2 ?B} log:implies {:g4 :gnand2
:a13} .
{?G = :g4. ?C = :a14. ?G :gnand3 ?C} log:implies {:g4 :gnand3
:a14} .
{{?G1 = :g2. ?G2 = :g4. ?G1 :nandnand1 ?G2} log:implies {:g2
:nandnand1 :g4} .
{?G1 = :g2. ?X = :a12. ?G1 :gnand3 ?X} log:implies {:g2 :gnand3
:a12} .
{?G2 = :g4. ?X = :a12. ?G2 :gnand1 ?X} log:implies {:g4 :gnand1
:a12} .
{{?G = :g2. ?A = :a. ?G :gnand1 ?A} log:implies {:g2 :gnand1
:a} .
{?G = :g2. ?B = :a11. ?G :gnand2 ?B} log:implies {:g2 :gnand2
:a11} .
{?G = :g2. ?C = :a12. ?G :gnand3 ?C} log:implies {:g2 :gnand3
:a12} .
{?A = :a. ?A :nand1 "true"} log:implies {:a :nand1 "true"} .
{{?G1 = :g1. ?G2 = :g2. ?G1 :nandnand2 ?G2} log:implies {:g1
:nandnand2 :g2} .
{?G1 = :g1. ?X = :a11. ?G1 :gnand3 ?X} log:implies {:g1
:gnand3 :a11} .
{?G2 = :g2. ?X = :a11. ?G2 :gnand2 ?X} log:implies {:g2
:gnand2 :a11} .
{{?G = :g1. ?A = :a. ?G :gnand1 ?A} log:implies {:g1
:gnand1 :a} .
{?G = :g1. ?B = :b. ?G :gnand2 ?B} log:implies {:g1
:gnand2 :b} .
{?G = :g1. ?C = :a11. ?G :gnand3 ?C} log:implies {:g1
:gnand3 :a11} .
{?A = :a. ?A :nand1 "true"} log:implies {:a :nand1
"true"} .
{?B = :b. ?B :nand2 "true"} log:implies {:b :nand2
"true"} .
?X = :a11. ?V = "false". ?X :nand3 ?V} log:implies
{:a11 :nand3 "false"} .
?B = :a11. ?B :nand2 "false"} log:implies
{:a11 :nand2 "false"} .
?X = :a12. ?V = "true". ?X :nand3 ?V} log:implies
{:a12 :nand3 "true"} .
?A = :a12. ?A :nand1 "true"} log:implies
{:a12 :nand1 "true"} .
{{?G1 = :g3. ?G2 = :g4. ?G1 :nandnand2 ?G2} log:implies {:g3
:nandnand2 :g4} .
{?G1 = :g3. ?X = :a13. ?G1 :gnand3 ?X} log:implies {:g3 :gnand3
:a13} .
{?G2 = :g4. ?X = :a13. ?G2 :gnand2 ?X} log:implies {:g4 :gnand2
:a13} .
{{?G = :g3. ?A = :a11. ?G :gnand1 ?A} log:implies {:g3 :gnand1
:a11} .
{?G = :g3. ?B = :b. ?G :gnand2 ?B} log:implies {:g3 :gnand2
:b} .
{?G = :g3. ?C = :a13. ?G :gnand3 ?C} log:implies {:g3 :gnand3
:a13} .
{{?G1 = :g1. ?G2 = :g3. ?G1 :nandnand1 ?G2} log:implies {:g1
:nandnand1 :g3} .
{?G1 = :g1. ?X = :a11. ?G1 :gnand3 ?X} log:implies {:g1
:gnand3 :a11} .
{?G2 = :g3. ?X = :a11. ?G2 :gnand1 ?X} log:implies {:g3
:gnand1 :a11} .
{{?G = :g1. ?A = :a. ?G :gnand1 ?A} log:implies {:g1
:gnand1 :a} .
{?G = :g1. ?B = :b. ?G :gnand2 ?B} log:implies {:g1
:gnand2 :b} .
{?G = :g1. ?C = :a11. ?G :gnand3 ?C} log:implies {:g1
:gnand3 :a11} .
{?A = :a. ?A :nand1 "true"} log:implies {:a :nand1
"true"} .
{?B = :b. ?B :nand2 "true"} log:implies {:b :nand2
"true"} .
?X = :a11. ?V = "false". ?X :nand3 ?V} log:implies
{:a11 :nand3 "false"} .
?A = :a11. ?A :nand1 "false"} log:implies
{:a11 :nand1 "false"} .
{?B = :b. ?B :nand2 "true"} log:implies {:b :nand2 "true"} .
?X = :a13. ?V = "true". ?X :nand3 ?V} log:implies
{:a13 :nand3 "true"} .
?B = :a13. ?B :nand2 "true"} log:implies
{:a13 :nand2 "true"} .
?X = :a14. ?V = "false". ?X :nand3 ?V} log:implies
{:a14 :nand3 "false"} .
?A = :a14. ?A :nand1 "false"} log:implies
{:a14 :nand1 "false"} .
{?B = :cin. ?B :nand2 "true"} log:implies {:cin :nand2 "true"} .
?X = :a15. ?V = "true". ?X :nand3 ?V} log:implies
{:a15 :nand3 "true"} .
?A = :a15. ?A :nand1 "true"} log:implies
{:a15 :nand1 "true"} .
{{?G1 = :g1. ?G2 = :g2. ?G1 :nandnand2 ?G2} log:implies {:g1 :nandnand2
:g2} .
{?G1 = :g1. ?X = :a11. ?G1 :gnand3 ?X} log:implies {:g1 :gnand3 :a11} .
{?G2 = :g2. ?X = :a11. ?G2 :gnand2 ?X} log:implies {:g2 :gnand2 :a11} .
{{?G = :g1. ?A = :a. ?G :gnand1 ?A} log:implies {:g1 :gnand1 :a} .
{?G = :g1. ?B = :b. ?G :gnand2 ?B} log:implies {:g1 :gnand2 :b} .
{?G = :g1. ?C = :a11. ?G :gnand3 ?C} log:implies {:g1 :gnand3 :a11} .
{?A = :a. ?A :nand1 "true"} log:implies {:a :nand1 "true"} .
{?B = :b. ?B :nand2 "true"} log:implies {:b :nand2 "true"} .
?X = :a11. ?V = "false". ?X :nand3 ?V} log:implies
{:a11 :nand3 "false"} .
?B = :a11. ?B :nand2 "false"} log:implies
{:a11 :nand2 "false"} .
?V = "true". :cout :nand3 ?V} log:implies
{:cout :nand3 "true"} .
# Proof found for http://www.agfa.com/w3c/2002/02/thesis/booleW.q.n3 in
81311 steps (72494 steps/sec
) using 1 engine
-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Sunday, 30 March 2003 14:41:55 UTC