- From: <jos.deroo@agfa.com>
- Date: Fri, 8 Sep 2006 13:46:25 +0200
- To: www-archive@w3.org
python check.py http://eulersharp.sourceforge.net/2006/02swap/gedcomE.n3
for version $Id: check.py,v 1.55.2.1 2006/09/07 06:54:54 connolly Exp $
gives the following proof checking result:
@prefix : <http://www.agfa.com/w3c/euler/gedcom-facts#> .
:Dirk :testRelationship :Bart,
:Tom .
:Geert :testRelationship :Bart,
:Tom .
:Jos :testRelationship :Bart,
:Tom .
1: ...
[by parsing <gedcom-facts.n3>]
2: :Jos gc:childIn :dp .
[by CE on 1 (@@_g_L24C9)]
3: ...
[by parsing <gedcom-facts.n3>]
4: :Maria gc:spouseIn :dp .
[by CE on 3 (@@_g_L25C9)]
5: ...
[by parsing <gedcom-relations.n3>]
6: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 5 (@@_g_L29C16)]
7: :Jos gc:parent :Maria .
[by GMP on 6, [2, 4]]
8: :Jos gc:parent :Maria .
[by CE on 7 (@@_g_L23C7)]
9: ...
[by parsing <gedcom-facts.n3>]
10: <http://www.agfa.com/w3c/euler/gedcom-facts#Maria> :sex :Female .
[by CE on 9 (@@_g_L30C7)]
11: ...
[by parsing <gedcom-relations.n3>]
12: @forAll :C, :P . { :C gc:parent :P . :P gc:sex gc:Female . }
log:implies {:C gc:mother :P . } .
[by CE on 11 (@@_g_L33C14)]
13: :Jos gc:mother :Maria .
[by GMP on 12, [8, 10]]
14: :Jos gc:mother :Maria .
[by CE on 13 (@@_g_L22C5)]
15: ...
[by parsing <gedcom-facts.n3>]
16: :Rita gc:childIn :dp .
[by CE on 15 (@@_g_L36C9)]
17: ...
[by parsing <gedcom-facts.n3>]
18: :Maria gc:spouseIn :dp .
[by CE on 17 (@@_g_L37C9)]
19: ...
[by parsing <gedcom-relations.n3>]
20: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 19 (@@_g_L41C16)]
21: :Rita gc:parent :Maria .
[by GMP on 20, [16, 18]]
22: :Rita gc:parent :Maria .
[by CE on 21 (@@_g_L35C7)]
23: ...
[by parsing <gedcom-facts.n3>]
24: <http://www.agfa.com/w3c/euler/gedcom-facts#Rita> :sex :Female .
[by CE on 23 (@@_g_L42C7)]
25: ...
[by parsing <gedcom-relations.n3>]
26: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Female . } log:implies
{:P gc:daughter :C . } .
[by CE on 25 (@@_g_L45C14)]
27: :Maria gc:daughter :Rita .
[by GMP on 26, [22, 24]]
28: :Maria gc:daughter :Rita .
[by CE on 27 (@@_g_L34C5)]
29: ...
[by parsing <gedcom-facts.n3>]
30: :Bart gc:childIn :gd .
[by CE on 29 (@@_g_L48C9)]
31: ...
[by parsing <gedcom-facts.n3>]
32: :Rita gc:spouseIn :gd .
[by CE on 31 (@@_g_L49C9)]
33: ...
[by parsing <gedcom-relations.n3>]
34: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 33 (@@_g_L53C16)]
35: :Bart gc:parent :Rita .
[by GMP on 34, [30, 32]]
36: :Bart gc:parent :Rita .
[by CE on 35 (@@_g_L47C7)]
37: ...
[by parsing <gedcom-facts.n3>]
38: <http://www.agfa.com/w3c/euler/gedcom-facts#Bart> :sex :Male .
[by CE on 37 (@@_g_L54C7)]
39: ...
[by parsing <gedcom-relations.n3>]
40: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Male . } log:implies {:P
gc:son :C . } .
[by CE on 39 (@@_g_L57C14)]
41: :Rita gc:son :Bart .
[by GMP on 40, [36, 38]]
42: :Rita gc:son :Bart .
[by CE on 41 (@@_g_L46C5)]
43: ...
[by parsing <gedcom-facts.n3>]
44: :Bart gc:childIn :gd .
[by CE on 43 (@@_g_L60C9)]
45: ...
[by parsing <gedcom-facts.n3>]
46: :Rita gc:spouseIn :gd .
[by CE on 45 (@@_g_L61C9)]
47: ...
[by parsing <gedcom-relations.n3>]
48: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 47 (@@_g_L65C16)]
49: :Bart gc:parent :Rita .
[by GMP on 48, [44, 46]]
50: :Bart gc:parent :Rita .
[by CE on 49 (@@_g_L59C7)]
51: ...
[by parsing <gedcom-relations.n3>]
52: :sibling a owl:SymmetricProperty .
[by CE on 51 (@@_g_L68C11)]
53: ...
[by parsing <gedcom-facts.n3>]
54: :Jos gc:childIn :dp .
[by CE on 53 (@@_g_L70C13)]
55: ...
[by parsing <gedcom-facts.n3>]
56: :Rita gc:childIn :dp .
[by CE on 55 (@@_g_L71C13)]
57: ...
[by parsing <gedcom-facts.n3>]
58: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by CE on 57 (@@_g_L73C15)]
59: ...
[by parsing <rpo-rules.n3>]
60: owl:distinctMembers :range rdf:List .
[by CE on 59 (@@_g_L76C19)]
61: ...
[by parsing <gedcom-facts.n3>]
62: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by CE on 61 (@@_g_L77C19)]
63: ...
[by parsing <rpo-rules.n3>]
64: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . } log:implies
{:O a :C . } .
[by CE on 63 (@@_g_L82C26)]
65: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 64, [60, 62]]
66: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 65 (@@_g_L75C17)]
67: ...
[by parsing <rpo-rules.n3>]
68: @forAll :L . { :L a rdf:List . } log:implies {:L p0:subListOf :L . } .
[by CE on 67 (@@_g_L84C24)]
69: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita
:Geert :Caroline :Dirk :Greta ) .
[by GMP on 68, [66]]
70: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita
:Geert :Caroline :Dirk :Greta ) .
[by CE on 69 (@@_g_L74C15)]
71: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
72: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
73: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
74: ...
[by parsing <rpo-rules.n3>]
75: rdf:rest :range rdf:List .
[by CE on 74 (@@_g_L90C19)]
76: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
77: ...
[by parsing <rpo-rules.n3>]
78: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . } log:implies
{:O a :C . } .
[by CE on 77 (@@_g_L96C26)]
79: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 78, [75, 76]]
80: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 79 (@@_g_L89C17)]
81: ...
[by parsing <rpo-rules.n3>]
82: @forAll :I, :L . { :L a rdf:List; rdf:first :I . } log:implies {:I
list:in :L . } .
[by CE on 81 (@@_g_L99C24)]
83: :Rita list:in ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by GMP on 82, [73, 80]]
84: :Rita list:in ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by CE on 83 (@@_g_L87C15)]
85: ...
[by parsing <rpo-rules.n3>]
86: @forAll :A, :D, :L, :R, :X, :Y . { :A owl:distinctMembers :D . :L
p0:subListOf :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies
{:X owl:differentFrom :Y . } .
[by CE on 85 (@@_g_L106C22)]
87: :Jos owl:differentFrom :Rita .
[by GMP on 86, [58, 70, 71, 72, 84]]
88: :Jos owl:differentFrom :Rita .
[by CE on 87 (@@_g_L72C13)]
89: ...
[by parsing <gedcom-relations.n3>]
90: @forAll :C, :C2, :F . { :C gc:childIn :F; owl:differentFrom :C2 . :C2
gc:childIn :F . } log:implies {:C gc:sibling :C2 . } .
[by CE on 89 (@@_g_L110C20)]
91: :Jos gc:sibling :Rita .
[by GMP on 90, [54, 56, 88]]
92: :Jos gc:sibling :Rita .
[by CE on 91 (@@_g_L69C11)]
93: ...
[by parsing <rpo-rules.n3>]
94: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . }
log:implies {:O :P :S . } .
[by CE on 93 (@@_g_L114C18)]
95: :Rita gc:sibling :Jos .
[by GMP on 94, [52, 92]]
96: :Rita gc:sibling :Jos .
[by CE on 95 (@@_g_L67C9)]
97: ...
[by parsing <gedcom-facts.n3>]
98: <http://www.agfa.com/w3c/euler/gedcom-facts#Jos> :sex :Male .
[by CE on 97 (@@_g_L115C9)]
99: ...
[by parsing <gedcom-relations.n3>]
100: @forAll :C, :S . { :C gc:sibling :S . :S gc:sex gc:Male . }
log:implies {:C gc:brother :S . } .
[by CE on 99 (@@_g_L118C16)]
101: :Rita gc:brother :Jos .
[by GMP on 100, [96, 98]]
102: :Rita gc:brother :Jos .
[by CE on 101 (@@_g_L66C7)]
103: ...
[by parsing <gedcom-relations.n3>]
104: @forAll :C, :P, :U . { :C gc:parent :P . :P gc:brother :U . }
log:implies {:C gc:uncle :U . } .
[by CE on 103 (@@_g_L122C14)]
105: :Bart gc:uncle :Jos .
[by GMP on 104, [50, 102]]
106: :Bart gc:uncle :Jos .
[by CE on 105 (@@_g_L58C5)]
107: ...
[by parsing <gedcom-filter.n3>]
108: @forAll :A, :D, :M, :S . { :A gc:mother :M . :D gc:son :S . :M
gc:daughter :D . :S gc:uncle :A . } log:implies {:A
<http://www.agfa.com/w3c/euler/gedcom-facts#testRelationship> :S . } .
[by CE on 107 (@@_g_L127C12)]
109: :Jos :testRelationship :Bart .
[by GMP on 108, [14, 28, 42, 106]]
110: ...
[by parsing <gedcom-facts.n3>]
111: :Geert gc:childIn :dp .
[by CE on 110 (@@_g_L131C9)]
112: ...
[by parsing <gedcom-facts.n3>]
113: :Maria gc:spouseIn :dp .
[by CE on 112 (@@_g_L132C9)]
114: ...
[by parsing <gedcom-relations.n3>]
115: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 114 (@@_g_L136C16)]
116: :Geert gc:parent :Maria .
[by GMP on 115, [111, 113]]
117: :Geert gc:parent :Maria .
[by CE on 116 (@@_g_L130C7)]
118: ...
[by parsing <gedcom-facts.n3>]
119: <http://www.agfa.com/w3c/euler/gedcom-facts#Maria> :sex :Female .
[by CE on 118 (@@_g_L137C7)]
120: ...
[by parsing <gedcom-relations.n3>]
121: @forAll :C, :P . { :C gc:parent :P . :P gc:sex gc:Female . }
log:implies {:C gc:mother :P . } .
[by CE on 120 (@@_g_L140C14)]
122: :Geert gc:mother :Maria .
[by GMP on 121, [117, 119]]
123: :Geert gc:mother :Maria .
[by CE on 122 (@@_g_L129C5)]
124: ...
[by parsing <gedcom-facts.n3>]
125: :Rita gc:childIn :dp .
[by CE on 124 (@@_g_L143C9)]
126: ...
[by parsing <gedcom-facts.n3>]
127: :Maria gc:spouseIn :dp .
[by CE on 126 (@@_g_L144C9)]
128: ...
[by parsing <gedcom-relations.n3>]
129: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 128 (@@_g_L148C16)]
130: :Rita gc:parent :Maria .
[by GMP on 129, [125, 127]]
131: :Rita gc:parent :Maria .
[by CE on 130 (@@_g_L142C7)]
132: ...
[by parsing <gedcom-facts.n3>]
133: <http://www.agfa.com/w3c/euler/gedcom-facts#Rita> :sex :Female .
[by CE on 132 (@@_g_L149C7)]
134: ...
[by parsing <gedcom-relations.n3>]
135: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Female . } log:implies
{:P gc:daughter :C . } .
[by CE on 134 (@@_g_L152C14)]
136: :Maria gc:daughter :Rita .
[by GMP on 135, [131, 133]]
137: :Maria gc:daughter :Rita .
[by CE on 136 (@@_g_L141C5)]
138: ...
[by parsing <gedcom-facts.n3>]
139: :Bart gc:childIn :gd .
[by CE on 138 (@@_g_L155C9)]
140: ...
[by parsing <gedcom-facts.n3>]
141: :Rita gc:spouseIn :gd .
[by CE on 140 (@@_g_L156C9)]
142: ...
[by parsing <gedcom-relations.n3>]
143: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 142 (@@_g_L160C16)]
144: :Bart gc:parent :Rita .
[by GMP on 143, [139, 141]]
145: :Bart gc:parent :Rita .
[by CE on 144 (@@_g_L154C7)]
146: ...
[by parsing <gedcom-facts.n3>]
147: <http://www.agfa.com/w3c/euler/gedcom-facts#Bart> :sex :Male .
[by CE on 146 (@@_g_L161C7)]
148: ...
[by parsing <gedcom-relations.n3>]
149: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Male . } log:implies
{:P gc:son :C . } .
[by CE on 148 (@@_g_L164C14)]
150: :Rita gc:son :Bart .
[by GMP on 149, [145, 147]]
151: :Rita gc:son :Bart .
[by CE on 150 (@@_g_L153C5)]
152: ...
[by parsing <gedcom-facts.n3>]
153: :Bart gc:childIn :gd .
[by CE on 152 (@@_g_L167C9)]
154: ...
[by parsing <gedcom-facts.n3>]
155: :Rita gc:spouseIn :gd .
[by CE on 154 (@@_g_L168C9)]
156: ...
[by parsing <gedcom-relations.n3>]
157: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 156 (@@_g_L172C16)]
158: :Bart gc:parent :Rita .
[by GMP on 157, [153, 155]]
159: :Bart gc:parent :Rita .
[by CE on 158 (@@_g_L166C7)]
160: ...
[by parsing <gedcom-facts.n3>]
161: :Rita gc:childIn :dp .
[by CE on 160 (@@_g_L175C11)]
162: ...
[by parsing <gedcom-facts.n3>]
163: :Geert gc:childIn :dp .
[by CE on 162 (@@_g_L176C11)]
164: ...
[by parsing <gedcom-facts.n3>]
165: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 164 (@@_g_L178C13)]
166: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
167: ...
[by parsing <rpo-rules.n3>]
168: owl:distinctMembers :range rdf:List .
[by CE on 167 (@@_g_L182C17)]
169: ...
[by parsing <gedcom-facts.n3>]
170: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 169 (@@_g_L183C17)]
171: ...
[by parsing <rpo-rules.n3>]
172: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 171 (@@_g_L188C24)]
173: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 172, [168, 170]]
174: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 173 (@@_g_L181C15)]
175: ...
[by parsing <rpo-rules.n3>]
176: rdf:rest :range rdf:List .
[by CE on 175 (@@_g_L191C19)]
177: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
178: ...
[by parsing <rpo-rules.n3>]
179: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 178 (@@_g_L197C26)]
180: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 179, [176, 177]]
181: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 180 (@@_g_L190C17)]
182: ...
[by parsing <rpo-rules.n3>]
183: @forAll :L . { :L a rdf:List . } log:implies {:L p0:subListOf :L . }
.
[by CE on 182 (@@_g_L199C24)]
184: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Rita :Geert
:Caroline :Dirk :Greta ) .
[by GMP on 183, [181]]
185: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Rita :Geert
:Caroline :Dirk :Greta ) .
[by CE on 184 (@@_g_L189C15)]
186: ...
[by parsing <rpo-rules.n3>]
187: @forAll :L, :R, :X . { :L a rdf:List; rdf:rest :R . :X p0:subListOf
:R . } log:implies {:X p0:subListOf :L . } .
[by CE on 186 (@@_g_L203C22)]
188: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita
:Geert :Caroline :Dirk :Greta ) .
[by GMP on 187, [166, 174, 185]]
189: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita
:Geert :Caroline :Dirk :Greta ) .
[by CE on 188 (@@_g_L179C13)]
190: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
191: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
192: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
193: ...
[by parsing <rpo-rules.n3>]
194: rdf:rest :range rdf:List .
[by CE on 193 (@@_g_L209C17)]
195: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
196: ...
[by parsing <rpo-rules.n3>]
197: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 196 (@@_g_L215C24)]
198: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 197, [194, 195]]
199: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 198 (@@_g_L208C15)]
200: ...
[by parsing <rpo-rules.n3>]
201: @forAll :I, :L . { :L a rdf:List; rdf:first :I . } log:implies {:I
list:in :L . } .
[by CE on 200 (@@_g_L218C22)]
202: :Geert list:in ( :Geert :Caroline :Dirk :Greta ) .
[by GMP on 201, [192, 199]]
203: :Geert list:in ( :Geert :Caroline :Dirk :Greta ) .
[by CE on 202 (@@_g_L206C13)]
204: ...
[by parsing <rpo-rules.n3>]
205: @forAll :A, :D, :L, :R, :X, :Y . { :A owl:distinctMembers :D . :L
p0:subListOf :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies
{:X owl:differentFrom :Y . } .
[by CE on 204 (@@_g_L225C20)]
206: :Rita owl:differentFrom :Geert .
[by GMP on 205, [165, 189, 190, 191, 203]]
207: :Rita owl:differentFrom :Geert .
[by CE on 206 (@@_g_L177C11)]
208: ...
[by parsing <gedcom-relations.n3>]
209: @forAll :C, :C2, :F . { :C gc:childIn :F; owl:differentFrom :C2 . :C2
gc:childIn :F . } log:implies {:C gc:sibling :C2 . } .
[by CE on 208 (@@_g_L229C18)]
210: :Rita gc:sibling :Geert .
[by GMP on 209, [161, 163, 207]]
211: :Rita gc:sibling :Geert .
[by CE on 210 (@@_g_L174C9)]
212: ...
[by parsing <gedcom-facts.n3>]
213: <http://www.agfa.com/w3c/euler/gedcom-facts#Geert> :sex :Male .
[by CE on 212 (@@_g_L230C9)]
214: ...
[by parsing <gedcom-relations.n3>]
215: @forAll :C, :S . { :C gc:sibling :S . :S gc:sex gc:Male . }
log:implies {:C gc:brother :S . } .
[by CE on 214 (@@_g_L233C16)]
216: :Rita gc:brother :Geert .
[by GMP on 215, [211, 213]]
217: :Rita gc:brother :Geert .
[by CE on 216 (@@_g_L173C7)]
218: ...
[by parsing <gedcom-relations.n3>]
219: @forAll :C, :P, :U . { :C gc:parent :P . :P gc:brother :U . }
log:implies {:C gc:uncle :U . } .
[by CE on 218 (@@_g_L237C14)]
220: :Bart gc:uncle :Geert .
[by GMP on 219, [159, 217]]
221: :Bart gc:uncle :Geert .
[by CE on 220 (@@_g_L165C5)]
222: ...
[by parsing <gedcom-filter.n3>]
223: @forAll :A, :D, :M, :S . { :A gc:mother :M . :D gc:son :S . :M
gc:daughter :D . :S gc:uncle :A . } log:implies {:A
<http://www.agfa.com/w3c/euler/gedcom-facts#testRelationship> :S . } .
[by CE on 222 (@@_g_L242C12)]
224: :Geert :testRelationship :Bart .
[by GMP on 223, [123, 137, 151, 221]]
225: ...
[by parsing <gedcom-facts.n3>]
226: :Dirk gc:childIn :dp .
[by CE on 225 (@@_g_L246C9)]
227: ...
[by parsing <gedcom-facts.n3>]
228: :Maria gc:spouseIn :dp .
[by CE on 227 (@@_g_L247C9)]
229: ...
[by parsing <gedcom-relations.n3>]
230: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 229 (@@_g_L251C16)]
231: :Dirk gc:parent :Maria .
[by GMP on 230, [226, 228]]
232: :Dirk gc:parent :Maria .
[by CE on 231 (@@_g_L245C7)]
233: ...
[by parsing <gedcom-facts.n3>]
234: <http://www.agfa.com/w3c/euler/gedcom-facts#Maria> :sex :Female .
[by CE on 233 (@@_g_L252C7)]
235: ...
[by parsing <gedcom-relations.n3>]
236: @forAll :C, :P . { :C gc:parent :P . :P gc:sex gc:Female . }
log:implies {:C gc:mother :P . } .
[by CE on 235 (@@_g_L255C14)]
237: :Dirk gc:mother :Maria .
[by GMP on 236, [232, 234]]
238: :Dirk gc:mother :Maria .
[by CE on 237 (@@_g_L244C5)]
239: ...
[by parsing <gedcom-facts.n3>]
240: :Rita gc:childIn :dp .
[by CE on 239 (@@_g_L258C9)]
241: ...
[by parsing <gedcom-facts.n3>]
242: :Maria gc:spouseIn :dp .
[by CE on 241 (@@_g_L259C9)]
243: ...
[by parsing <gedcom-relations.n3>]
244: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 243 (@@_g_L263C16)]
245: :Rita gc:parent :Maria .
[by GMP on 244, [240, 242]]
246: :Rita gc:parent :Maria .
[by CE on 245 (@@_g_L257C7)]
247: ...
[by parsing <gedcom-facts.n3>]
248: <http://www.agfa.com/w3c/euler/gedcom-facts#Rita> :sex :Female .
[by CE on 247 (@@_g_L264C7)]
249: ...
[by parsing <gedcom-relations.n3>]
250: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Female . } log:implies
{:P gc:daughter :C . } .
[by CE on 249 (@@_g_L267C14)]
251: :Maria gc:daughter :Rita .
[by GMP on 250, [246, 248]]
252: :Maria gc:daughter :Rita .
[by CE on 251 (@@_g_L256C5)]
253: ...
[by parsing <gedcom-facts.n3>]
254: :Bart gc:childIn :gd .
[by CE on 253 (@@_g_L270C9)]
255: ...
[by parsing <gedcom-facts.n3>]
256: :Rita gc:spouseIn :gd .
[by CE on 255 (@@_g_L271C9)]
257: ...
[by parsing <gedcom-relations.n3>]
258: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 257 (@@_g_L275C16)]
259: :Bart gc:parent :Rita .
[by GMP on 258, [254, 256]]
260: :Bart gc:parent :Rita .
[by CE on 259 (@@_g_L269C7)]
261: ...
[by parsing <gedcom-facts.n3>]
262: <http://www.agfa.com/w3c/euler/gedcom-facts#Bart> :sex :Male .
[by CE on 261 (@@_g_L276C7)]
263: ...
[by parsing <gedcom-relations.n3>]
264: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Male . } log:implies
{:P gc:son :C . } .
[by CE on 263 (@@_g_L279C14)]
265: :Rita gc:son :Bart .
[by GMP on 264, [260, 262]]
266: :Rita gc:son :Bart .
[by CE on 265 (@@_g_L268C5)]
267: ...
[by parsing <gedcom-facts.n3>]
268: :Bart gc:childIn :gd .
[by CE on 267 (@@_g_L282C9)]
269: ...
[by parsing <gedcom-facts.n3>]
270: :Rita gc:spouseIn :gd .
[by CE on 269 (@@_g_L283C9)]
271: ...
[by parsing <gedcom-relations.n3>]
272: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 271 (@@_g_L287C16)]
273: :Bart gc:parent :Rita .
[by GMP on 272, [268, 270]]
274: :Bart gc:parent :Rita .
[by CE on 273 (@@_g_L281C7)]
275: ...
[by parsing <gedcom-facts.n3>]
276: :Rita gc:childIn :dp .
[by CE on 275 (@@_g_L290C11)]
277: ...
[by parsing <gedcom-facts.n3>]
278: :Dirk gc:childIn :dp .
[by CE on 277 (@@_g_L291C11)]
279: ...
[by parsing <gedcom-facts.n3>]
280: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 279 (@@_g_L293C13)]
281: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
282: ...
[by parsing <rpo-rules.n3>]
283: owl:distinctMembers :range rdf:List .
[by CE on 282 (@@_g_L297C17)]
284: ...
[by parsing <gedcom-facts.n3>]
285: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 284 (@@_g_L298C17)]
286: ...
[by parsing <rpo-rules.n3>]
287: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 286 (@@_g_L303C24)]
288: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 287, [283, 285]]
289: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 288 (@@_g_L296C15)]
290: ...
[by parsing <rpo-rules.n3>]
291: rdf:rest :range rdf:List .
[by CE on 290 (@@_g_L306C19)]
292: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
293: ...
[by parsing <rpo-rules.n3>]
294: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 293 (@@_g_L312C26)]
295: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 294, [291, 292]]
296: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 295 (@@_g_L305C17)]
297: ...
[by parsing <rpo-rules.n3>]
298: @forAll :L . { :L a rdf:List . } log:implies {:L p0:subListOf :L . }
.
[by CE on 297 (@@_g_L314C24)]
299: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Rita :Geert
:Caroline :Dirk :Greta ) .
[by GMP on 298, [296]]
300: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Rita :Geert
:Caroline :Dirk :Greta ) .
[by CE on 299 (@@_g_L304C15)]
301: ...
[by parsing <rpo-rules.n3>]
302: @forAll :L, :R, :X . { :L a rdf:List; rdf:rest :R . :X p0:subListOf
:R . } log:implies {:X p0:subListOf :L . } .
[by CE on 301 (@@_g_L318C22)]
303: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita
:Geert :Caroline :Dirk :Greta ) .
[by GMP on 302, [281, 289, 300]]
304: ( :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita
:Geert :Caroline :Dirk :Greta ) .
[by CE on 303 (@@_g_L294C13)]
305: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
306: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
307: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
308: ...
[by parsing <rpo-rules.n3>]
309: rdf:rest :range rdf:List .
[by CE on 308 (@@_g_L324C17)]
310: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
311: ...
[by parsing <rpo-rules.n3>]
312: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 311 (@@_g_L330C24)]
313: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 312, [309, 310]]
314: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 313 (@@_g_L323C15)]
315: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
316: ...
[by parsing <rpo-rules.n3>]
317: rdf:rest :range rdf:List .
[by CE on 316 (@@_g_L334C19)]
318: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
319: ...
[by parsing <rpo-rules.n3>]
320: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 319 (@@_g_L340C26)]
321: ( :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 320, [317, 318]]
322: ( :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 321 (@@_g_L333C17)]
323: ( :Dirk :Greta ) .
[by built-in Axiom rdf:first]
324: ...
[by parsing <rpo-rules.n3>]
325: rdf:rest :range rdf:List .
[by CE on 324 (@@_g_L344C21)]
326: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
327: ...
[by parsing <rpo-rules.n3>]
328: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 327 (@@_g_L350C28)]
329: ( :Dirk :Greta ) a rdf:List .
[by GMP on 328, [325, 326]]
330: ( :Dirk :Greta ) a rdf:List .
[by CE on 329 (@@_g_L343C19)]
331: ...
[by parsing <rpo-rules.n3>]
332: @forAll :I, :L . { :L a rdf:List; rdf:first :I . } log:implies {:I
list:in :L . } .
[by CE on 331 (@@_g_L353C26)]
333: :Dirk list:in ( :Dirk :Greta ) .
[by GMP on 332, [323, 330]]
334: :Dirk list:in ( :Dirk :Greta ) .
[by CE on 333 (@@_g_L341C17)]
335: ...
[by parsing <rpo-rules.n3>]
336: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 335 (@@_g_L357C24)]
337: :Dirk list:in ( :Caroline :Dirk :Greta ) .
[by GMP on 336, [315, 322, 334]]
338: :Dirk list:in ( :Caroline :Dirk :Greta ) .
[by CE on 337 (@@_g_L331C15)]
339: ...
[by parsing <rpo-rules.n3>]
340: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 339 (@@_g_L361C22)]
341: :Dirk list:in ( :Geert :Caroline :Dirk :Greta ) .
[by GMP on 340, [307, 314, 338]]
342: :Dirk list:in ( :Geert :Caroline :Dirk :Greta ) .
[by CE on 341 (@@_g_L321C13)]
343: ...
[by parsing <rpo-rules.n3>]
344: @forAll :A, :D, :L, :R, :X, :Y . { :A owl:distinctMembers :D . :L
p0:subListOf :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies
{:X owl:differentFrom :Y . } .
[by CE on 343 (@@_g_L368C20)]
345: :Rita owl:differentFrom :Dirk .
[by GMP on 344, [280, 304, 305, 306, 342]]
346: :Rita owl:differentFrom :Dirk .
[by CE on 345 (@@_g_L292C11)]
347: ...
[by parsing <gedcom-relations.n3>]
348: @forAll :C, :C2, :F . { :C gc:childIn :F; owl:differentFrom :C2 . :C2
gc:childIn :F . } log:implies {:C gc:sibling :C2 . } .
[by CE on 347 (@@_g_L372C18)]
349: :Rita gc:sibling :Dirk .
[by GMP on 348, [276, 278, 346]]
350: :Rita gc:sibling :Dirk .
[by CE on 349 (@@_g_L289C9)]
351: ...
[by parsing <gedcom-facts.n3>]
352: <http://www.agfa.com/w3c/euler/gedcom-facts#Dirk> :sex :Male .
[by CE on 351 (@@_g_L373C9)]
353: ...
[by parsing <gedcom-relations.n3>]
354: @forAll :C, :S . { :C gc:sibling :S . :S gc:sex gc:Male . }
log:implies {:C gc:brother :S . } .
[by CE on 353 (@@_g_L376C16)]
355: :Rita gc:brother :Dirk .
[by GMP on 354, [350, 352]]
356: :Rita gc:brother :Dirk .
[by CE on 355 (@@_g_L288C7)]
357: ...
[by parsing <gedcom-relations.n3>]
358: @forAll :C, :P, :U . { :C gc:parent :P . :P gc:brother :U . }
log:implies {:C gc:uncle :U . } .
[by CE on 357 (@@_g_L380C14)]
359: :Bart gc:uncle :Dirk .
[by GMP on 358, [274, 356]]
360: :Bart gc:uncle :Dirk .
[by CE on 359 (@@_g_L280C5)]
361: ...
[by parsing <gedcom-filter.n3>]
362: @forAll :A, :D, :M, :S . { :A gc:mother :M . :D gc:son :S . :M
gc:daughter :D . :S gc:uncle :A . } log:implies {:A
<http://www.agfa.com/w3c/euler/gedcom-facts#testRelationship> :S . } .
[by CE on 361 (@@_g_L385C12)]
363: :Dirk :testRelationship :Bart .
[by GMP on 362, [238, 252, 266, 360]]
364: ...
[by parsing <gedcom-facts.n3>]
365: :Dirk gc:childIn :dp .
[by CE on 364 (@@_g_L389C9)]
366: ...
[by parsing <gedcom-facts.n3>]
367: :Maria gc:spouseIn :dp .
[by CE on 366 (@@_g_L390C9)]
368: ...
[by parsing <gedcom-relations.n3>]
369: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 368 (@@_g_L394C16)]
370: :Dirk gc:parent :Maria .
[by GMP on 369, [365, 367]]
371: :Dirk gc:parent :Maria .
[by CE on 370 (@@_g_L388C7)]
372: ...
[by parsing <gedcom-facts.n3>]
373: <http://www.agfa.com/w3c/euler/gedcom-facts#Maria> :sex :Female .
[by CE on 372 (@@_g_L395C7)]
374: ...
[by parsing <gedcom-relations.n3>]
375: @forAll :C, :P . { :C gc:parent :P . :P gc:sex gc:Female . }
log:implies {:C gc:mother :P . } .
[by CE on 374 (@@_g_L398C14)]
376: :Dirk gc:mother :Maria .
[by GMP on 375, [371, 373]]
377: :Dirk gc:mother :Maria .
[by CE on 376 (@@_g_L387C5)]
378: ...
[by parsing <gedcom-facts.n3>]
379: :Greta gc:childIn :dp .
[by CE on 378 (@@_g_L401C9)]
380: ...
[by parsing <gedcom-facts.n3>]
381: :Maria gc:spouseIn :dp .
[by CE on 380 (@@_g_L402C9)]
382: ...
[by parsing <gedcom-relations.n3>]
383: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 382 (@@_g_L406C16)]
384: :Greta gc:parent :Maria .
[by GMP on 383, [379, 381]]
385: :Greta gc:parent :Maria .
[by CE on 384 (@@_g_L400C7)]
386: ...
[by parsing <gedcom-facts.n3>]
387: <http://www.agfa.com/w3c/euler/gedcom-facts#Greta> :sex :Female .
[by CE on 386 (@@_g_L407C7)]
388: ...
[by parsing <gedcom-relations.n3>]
389: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Female . } log:implies
{:P gc:daughter :C . } .
[by CE on 388 (@@_g_L410C14)]
390: :Maria gc:daughter :Greta .
[by GMP on 389, [385, 387]]
391: :Maria gc:daughter :Greta .
[by CE on 390 (@@_g_L399C5)]
392: ...
[by parsing <gedcom-facts.n3>]
393: :Tom gc:childIn :sd .
[by CE on 392 (@@_g_L413C9)]
394: ...
[by parsing <gedcom-facts.n3>]
395: :Greta gc:spouseIn :sd .
[by CE on 394 (@@_g_L414C9)]
396: ...
[by parsing <gedcom-relations.n3>]
397: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 396 (@@_g_L418C16)]
398: :Tom gc:parent :Greta .
[by GMP on 397, [393, 395]]
399: :Tom gc:parent :Greta .
[by CE on 398 (@@_g_L412C7)]
400: ...
[by parsing <gedcom-facts.n3>]
401: <http://www.agfa.com/w3c/euler/gedcom-facts#Tom> :sex :Male .
[by CE on 400 (@@_g_L419C7)]
402: ...
[by parsing <gedcom-relations.n3>]
403: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Male . } log:implies
{:P gc:son :C . } .
[by CE on 402 (@@_g_L422C14)]
404: :Greta gc:son :Tom .
[by GMP on 403, [399, 401]]
405: :Greta gc:son :Tom .
[by CE on 404 (@@_g_L411C5)]
406: ...
[by parsing <gedcom-facts.n3>]
407: :Tom gc:childIn :sd .
[by CE on 406 (@@_g_L425C9)]
408: ...
[by parsing <gedcom-facts.n3>]
409: :Greta gc:spouseIn :sd .
[by CE on 408 (@@_g_L426C9)]
410: ...
[by parsing <gedcom-relations.n3>]
411: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 410 (@@_g_L430C16)]
412: :Tom gc:parent :Greta .
[by GMP on 411, [407, 409]]
413: :Tom gc:parent :Greta .
[by CE on 412 (@@_g_L424C7)]
414: ...
[by parsing <gedcom-relations.n3>]
415: :sibling a owl:SymmetricProperty .
[by CE on 414 (@@_g_L433C11)]
416: ...
[by parsing <gedcom-facts.n3>]
417: :Dirk gc:childIn :dp .
[by CE on 416 (@@_g_L435C13)]
418: ...
[by parsing <gedcom-facts.n3>]
419: :Greta gc:childIn :dp .
[by CE on 418 (@@_g_L436C13)]
420: ...
[by parsing <gedcom-facts.n3>]
421: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 420 (@@_g_L440C19)]
422: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
423: ...
[by parsing <rpo-rules.n3>]
424: @forAll :A, :D, :R . { :A owl:distinctMembers :D . :D rdf:rest :R . }
log:implies {:A owl:distinctMembers :R . } .
[by CE on 423 (@@_g_L445C26)]
425: :dp owl:distinctMembers ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by GMP on 424, [421, 422]]
426: :dp owl:distinctMembers ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by CE on 425 (@@_g_L439C17)]
427: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
428: ...
[by parsing <rpo-rules.n3>]
429: @forAll :A, :D, :R . { :A owl:distinctMembers :D . :D rdf:rest :R . }
log:implies {:A owl:distinctMembers :R . } .
[by CE on 428 (@@_g_L450C24)]
430: :dp owl:distinctMembers ( :Geert :Caroline :Dirk :Greta ) .
[by GMP on 429, [426, 427]]
431: :dp owl:distinctMembers ( :Geert :Caroline :Dirk :Greta ) .
[by CE on 430 (@@_g_L438C15)]
432: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
433: ...
[by parsing <rpo-rules.n3>]
434: rdf:rest :range rdf:List .
[by CE on 433 (@@_g_L454C19)]
435: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
436: ...
[by parsing <rpo-rules.n3>]
437: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 436 (@@_g_L460C26)]
438: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 437, [434, 435]]
439: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 438 (@@_g_L453C17)]
440: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
441: ...
[by parsing <rpo-rules.n3>]
442: rdf:rest :range rdf:List .
[by CE on 441 (@@_g_L464C21)]
443: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
444: ...
[by parsing <rpo-rules.n3>]
445: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 444 (@@_g_L470C28)]
446: ( :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 445, [442, 443]]
447: ( :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 446 (@@_g_L463C19)]
448: ...
[by parsing <rpo-rules.n3>]
449: rdf:rest :range rdf:List .
[by CE on 448 (@@_g_L473C23)]
450: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
451: ...
[by parsing <rpo-rules.n3>]
452: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 451 (@@_g_L479C30)]
453: ( :Dirk :Greta ) a rdf:List .
[by GMP on 452, [449, 450]]
454: ( :Dirk :Greta ) a rdf:List .
[by CE on 453 (@@_g_L472C21)]
455: ...
[by parsing <rpo-rules.n3>]
456: @forAll :L . { :L a rdf:List . } log:implies {:L p0:subListOf :L . }
.
[by CE on 455 (@@_g_L481C28)]
457: ( :Dirk :Greta ) p0:subListOf ( :Dirk :Greta ) .
[by GMP on 456, [454]]
458: ( :Dirk :Greta ) p0:subListOf ( :Dirk :Greta ) .
[by CE on 457 (@@_g_L471C19)]
459: ...
[by parsing <rpo-rules.n3>]
460: @forAll :L, :R, :X . { :L a rdf:List; rdf:rest :R . :X p0:subListOf
:R . } log:implies {:X p0:subListOf :L . } .
[by CE on 459 (@@_g_L485C26)]
461: ( :Dirk :Greta ) p0:subListOf ( :Caroline :Dirk :Greta ) .
[by GMP on 460, [440, 447, 458]]
462: ( :Dirk :Greta ) p0:subListOf ( :Caroline :Dirk :Greta ) .
[by CE on 461 (@@_g_L461C17)]
463: ...
[by parsing <rpo-rules.n3>]
464: @forAll :L, :R, :X . { :L a rdf:List; rdf:rest :R . :X p0:subListOf
:R . } log:implies {:X p0:subListOf :L . } .
[by CE on 463 (@@_g_L489C24)]
465: ( :Dirk :Greta ) p0:subListOf ( :Geert :Caroline :Dirk :Greta ) .
[by GMP on 464, [432, 439, 462]]
466: ( :Dirk :Greta ) p0:subListOf ( :Geert :Caroline :Dirk :Greta ) .
[by CE on 465 (@@_g_L451C15)]
467: ( :Dirk :Greta ) .
[by built-in Axiom rdf:first]
468: ( :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
469: ( :Greta ) .
[by built-in Axiom rdf:first]
470: ...
[by parsing <rpo-rules.n3>]
471: rdf:rest :range rdf:List .
[by CE on 470 (@@_g_L495C19)]
472: ( :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
473: ...
[by parsing <rpo-rules.n3>]
474: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 473 (@@_g_L501C26)]
475: ( :Greta ) a rdf:List .
[by GMP on 474, [471, 472]]
476: ( :Greta ) a rdf:List .
[by CE on 475 (@@_g_L494C17)]
477: ...
[by parsing <rpo-rules.n3>]
478: @forAll :I, :L . { :L a rdf:List; rdf:first :I . } log:implies {:I
list:in :L . } .
[by CE on 477 (@@_g_L504C24)]
479: :Greta list:in ( :Greta ) .
[by GMP on 478, [469, 476]]
480: :Greta list:in ( :Greta ) .
[by CE on 479 (@@_g_L492C15)]
481: ...
[by parsing <rpo-rules.n3>]
482: @forAll :A, :D, :L, :R, :X, :Y . { :A owl:distinctMembers :D . :L
p0:subListOf :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies
{:X owl:differentFrom :Y . } .
[by CE on 481 (@@_g_L511C22)]
483: :Dirk owl:differentFrom :Greta .
[by GMP on 482, [431, 466, 467, 468, 480]]
484: :Dirk owl:differentFrom :Greta .
[by CE on 483 (@@_g_L437C13)]
485: ...
[by parsing <gedcom-relations.n3>]
486: @forAll :C, :C2, :F . { :C gc:childIn :F; owl:differentFrom :C2 . :C2
gc:childIn :F . } log:implies {:C gc:sibling :C2 . } .
[by CE on 485 (@@_g_L515C20)]
487: :Dirk gc:sibling :Greta .
[by GMP on 486, [417, 419, 484]]
488: :Dirk gc:sibling :Greta .
[by CE on 487 (@@_g_L434C11)]
489: ...
[by parsing <rpo-rules.n3>]
490: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . }
log:implies {:O :P :S . } .
[by CE on 489 (@@_g_L519C18)]
491: :Greta gc:sibling :Dirk .
[by GMP on 490, [415, 488]]
492: :Greta gc:sibling :Dirk .
[by CE on 491 (@@_g_L432C9)]
493: ...
[by parsing <gedcom-facts.n3>]
494: <http://www.agfa.com/w3c/euler/gedcom-facts#Dirk> :sex :Male .
[by CE on 493 (@@_g_L520C9)]
495: ...
[by parsing <gedcom-relations.n3>]
496: @forAll :C, :S . { :C gc:sibling :S . :S gc:sex gc:Male . }
log:implies {:C gc:brother :S . } .
[by CE on 495 (@@_g_L523C16)]
497: :Greta gc:brother :Dirk .
[by GMP on 496, [492, 494]]
498: :Greta gc:brother :Dirk .
[by CE on 497 (@@_g_L431C7)]
499: ...
[by parsing <gedcom-relations.n3>]
500: @forAll :C, :P, :U . { :C gc:parent :P . :P gc:brother :U . }
log:implies {:C gc:uncle :U . } .
[by CE on 499 (@@_g_L527C14)]
501: :Tom gc:uncle :Dirk .
[by GMP on 500, [413, 498]]
502: :Tom gc:uncle :Dirk .
[by CE on 501 (@@_g_L423C5)]
503: ...
[by parsing <gedcom-filter.n3>]
504: @forAll :A, :D, :M, :S . { :A gc:mother :M . :D gc:son :S . :M
gc:daughter :D . :S gc:uncle :A . } log:implies {:A
<http://www.agfa.com/w3c/euler/gedcom-facts#testRelationship> :S . } .
[by CE on 503 (@@_g_L532C12)]
505: :Dirk :testRelationship :Tom .
[by GMP on 504, [377, 391, 405, 502]]
506: ...
[by parsing <gedcom-facts.n3>]
507: :Geert gc:childIn :dp .
[by CE on 506 (@@_g_L536C9)]
508: ...
[by parsing <gedcom-facts.n3>]
509: :Maria gc:spouseIn :dp .
[by CE on 508 (@@_g_L537C9)]
510: ...
[by parsing <gedcom-relations.n3>]
511: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 510 (@@_g_L541C16)]
512: :Geert gc:parent :Maria .
[by GMP on 511, [507, 509]]
513: :Geert gc:parent :Maria .
[by CE on 512 (@@_g_L535C7)]
514: ...
[by parsing <gedcom-facts.n3>]
515: <http://www.agfa.com/w3c/euler/gedcom-facts#Maria> :sex :Female .
[by CE on 514 (@@_g_L542C7)]
516: ...
[by parsing <gedcom-relations.n3>]
517: @forAll :C, :P . { :C gc:parent :P . :P gc:sex gc:Female . }
log:implies {:C gc:mother :P . } .
[by CE on 516 (@@_g_L545C14)]
518: :Geert gc:mother :Maria .
[by GMP on 517, [513, 515]]
519: :Geert gc:mother :Maria .
[by CE on 518 (@@_g_L534C5)]
520: ...
[by parsing <gedcom-facts.n3>]
521: :Greta gc:childIn :dp .
[by CE on 520 (@@_g_L548C9)]
522: ...
[by parsing <gedcom-facts.n3>]
523: :Maria gc:spouseIn :dp .
[by CE on 522 (@@_g_L549C9)]
524: ...
[by parsing <gedcom-relations.n3>]
525: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 524 (@@_g_L553C16)]
526: :Greta gc:parent :Maria .
[by GMP on 525, [521, 523]]
527: :Greta gc:parent :Maria .
[by CE on 526 (@@_g_L547C7)]
528: ...
[by parsing <gedcom-facts.n3>]
529: <http://www.agfa.com/w3c/euler/gedcom-facts#Greta> :sex :Female .
[by CE on 528 (@@_g_L554C7)]
530: ...
[by parsing <gedcom-relations.n3>]
531: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Female . } log:implies
{:P gc:daughter :C . } .
[by CE on 530 (@@_g_L557C14)]
532: :Maria gc:daughter :Greta .
[by GMP on 531, [527, 529]]
533: :Maria gc:daughter :Greta .
[by CE on 532 (@@_g_L546C5)]
534: ...
[by parsing <gedcom-facts.n3>]
535: :Tom gc:childIn :sd .
[by CE on 534 (@@_g_L560C9)]
536: ...
[by parsing <gedcom-facts.n3>]
537: :Greta gc:spouseIn :sd .
[by CE on 536 (@@_g_L561C9)]
538: ...
[by parsing <gedcom-relations.n3>]
539: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 538 (@@_g_L565C16)]
540: :Tom gc:parent :Greta .
[by GMP on 539, [535, 537]]
541: :Tom gc:parent :Greta .
[by CE on 540 (@@_g_L559C7)]
542: ...
[by parsing <gedcom-facts.n3>]
543: <http://www.agfa.com/w3c/euler/gedcom-facts#Tom> :sex :Male .
[by CE on 542 (@@_g_L566C7)]
544: ...
[by parsing <gedcom-relations.n3>]
545: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Male . } log:implies
{:P gc:son :C . } .
[by CE on 544 (@@_g_L569C14)]
546: :Greta gc:son :Tom .
[by GMP on 545, [541, 543]]
547: :Greta gc:son :Tom .
[by CE on 546 (@@_g_L558C5)]
548: ...
[by parsing <gedcom-facts.n3>]
549: :Tom gc:childIn :sd .
[by CE on 548 (@@_g_L572C9)]
550: ...
[by parsing <gedcom-facts.n3>]
551: :Greta gc:spouseIn :sd .
[by CE on 550 (@@_g_L573C9)]
552: ...
[by parsing <gedcom-relations.n3>]
553: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 552 (@@_g_L577C16)]
554: :Tom gc:parent :Greta .
[by GMP on 553, [549, 551]]
555: :Tom gc:parent :Greta .
[by CE on 554 (@@_g_L571C7)]
556: ...
[by parsing <gedcom-relations.n3>]
557: :sibling a owl:SymmetricProperty .
[by CE on 556 (@@_g_L580C11)]
558: ...
[by parsing <gedcom-facts.n3>]
559: :Geert gc:childIn :dp .
[by CE on 558 (@@_g_L582C13)]
560: ...
[by parsing <gedcom-facts.n3>]
561: :Greta gc:childIn :dp .
[by CE on 560 (@@_g_L583C13)]
562: ...
[by parsing <gedcom-facts.n3>]
563: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 562 (@@_g_L585C15)]
564: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
565: ...
[by parsing <rpo-rules.n3>]
566: owl:distinctMembers :range rdf:List .
[by CE on 565 (@@_g_L589C19)]
567: ...
[by parsing <gedcom-facts.n3>]
568: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 567 (@@_g_L590C19)]
569: ...
[by parsing <rpo-rules.n3>]
570: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 569 (@@_g_L595C26)]
571: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 570, [566, 568]]
572: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 571 (@@_g_L588C17)]
573: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
574: ...
[by parsing <rpo-rules.n3>]
575: rdf:rest :range rdf:List .
[by CE on 574 (@@_g_L599C21)]
576: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
577: ...
[by parsing <rpo-rules.n3>]
578: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 577 (@@_g_L605C28)]
579: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 578, [575, 576]]
580: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 579 (@@_g_L598C19)]
581: ...
[by parsing <rpo-rules.n3>]
582: rdf:rest :range rdf:List .
[by CE on 581 (@@_g_L608C23)]
583: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
584: ...
[by parsing <rpo-rules.n3>]
585: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 584 (@@_g_L614C30)]
586: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 585, [582, 583]]
587: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 586 (@@_g_L607C21)]
588: ...
[by parsing <rpo-rules.n3>]
589: @forAll :L . { :L a rdf:List . } log:implies {:L p0:subListOf :L . }
.
[by CE on 588 (@@_g_L616C28)]
590: ( :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Geert :Caroline
:Dirk :Greta ) .
[by GMP on 589, [587]]
591: ( :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Geert :Caroline
:Dirk :Greta ) .
[by CE on 590 (@@_g_L606C19)]
592: ...
[by parsing <rpo-rules.n3>]
593: @forAll :L, :R, :X . { :L a rdf:List; rdf:rest :R . :X p0:subListOf
:R . } log:implies {:X p0:subListOf :L . } .
[by CE on 592 (@@_g_L620C26)]
594: ( :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Rita :Geert
:Caroline :Dirk :Greta ) .
[by GMP on 593, [573, 580, 591]]
595: ( :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Rita :Geert
:Caroline :Dirk :Greta ) .
[by CE on 594 (@@_g_L596C17)]
596: ...
[by parsing <rpo-rules.n3>]
597: @forAll :L, :R, :X . { :L a rdf:List; rdf:rest :R . :X p0:subListOf
:R . } log:implies {:X p0:subListOf :L . } .
[by CE on 596 (@@_g_L624C24)]
598: ( :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita :Geert
:Caroline :Dirk :Greta ) .
[by GMP on 597, [564, 572, 595]]
599: ( :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos :Rita :Geert
:Caroline :Dirk :Greta ) .
[by CE on 598 (@@_g_L586C15)]
600: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
601: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
602: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
603: ...
[by parsing <rpo-rules.n3>]
604: rdf:rest :range rdf:List .
[by CE on 603 (@@_g_L630C19)]
605: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
606: ...
[by parsing <rpo-rules.n3>]
607: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 606 (@@_g_L636C26)]
608: ( :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 607, [604, 605]]
609: ( :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 608 (@@_g_L629C17)]
610: ( :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
611: ...
[by parsing <rpo-rules.n3>]
612: rdf:rest :range rdf:List .
[by CE on 611 (@@_g_L640C21)]
613: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
614: ...
[by parsing <rpo-rules.n3>]
615: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 614 (@@_g_L646C28)]
616: ( :Dirk :Greta ) a rdf:List .
[by GMP on 615, [612, 613]]
617: ( :Dirk :Greta ) a rdf:List .
[by CE on 616 (@@_g_L639C19)]
618: ( :Greta ) .
[by built-in Axiom rdf:first]
619: ...
[by parsing <rpo-rules.n3>]
620: rdf:rest :range rdf:List .
[by CE on 619 (@@_g_L650C23)]
621: ( :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
622: ...
[by parsing <rpo-rules.n3>]
623: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 622 (@@_g_L656C30)]
624: ( :Greta ) a rdf:List .
[by GMP on 623, [620, 621]]
625: ( :Greta ) a rdf:List .
[by CE on 624 (@@_g_L649C21)]
626: ...
[by parsing <rpo-rules.n3>]
627: @forAll :I, :L . { :L a rdf:List; rdf:first :I . } log:implies {:I
list:in :L . } .
[by CE on 626 (@@_g_L659C28)]
628: :Greta list:in ( :Greta ) .
[by GMP on 627, [618, 625]]
629: :Greta list:in ( :Greta ) .
[by CE on 628 (@@_g_L647C19)]
630: ...
[by parsing <rpo-rules.n3>]
631: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 630 (@@_g_L663C26)]
632: :Greta list:in ( :Dirk :Greta ) .
[by GMP on 631, [610, 617, 629]]
633: :Greta list:in ( :Dirk :Greta ) .
[by CE on 632 (@@_g_L637C17)]
634: ...
[by parsing <rpo-rules.n3>]
635: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 634 (@@_g_L667C24)]
636: :Greta list:in ( :Caroline :Dirk :Greta ) .
[by GMP on 635, [602, 609, 633]]
637: :Greta list:in ( :Caroline :Dirk :Greta ) .
[by CE on 636 (@@_g_L627C15)]
638: ...
[by parsing <rpo-rules.n3>]
639: @forAll :A, :D, :L, :R, :X, :Y . { :A owl:distinctMembers :D . :L
p0:subListOf :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies
{:X owl:differentFrom :Y . } .
[by CE on 638 (@@_g_L674C22)]
640: :Geert owl:differentFrom :Greta .
[by GMP on 639, [563, 599, 600, 601, 637]]
641: :Geert owl:differentFrom :Greta .
[by CE on 640 (@@_g_L584C13)]
642: ...
[by parsing <gedcom-relations.n3>]
643: @forAll :C, :C2, :F . { :C gc:childIn :F; owl:differentFrom :C2 . :C2
gc:childIn :F . } log:implies {:C gc:sibling :C2 . } .
[by CE on 642 (@@_g_L678C20)]
644: :Geert gc:sibling :Greta .
[by GMP on 643, [559, 561, 641]]
645: :Geert gc:sibling :Greta .
[by CE on 644 (@@_g_L581C11)]
646: ...
[by parsing <rpo-rules.n3>]
647: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . }
log:implies {:O :P :S . } .
[by CE on 646 (@@_g_L682C18)]
648: :Greta gc:sibling :Geert .
[by GMP on 647, [557, 645]]
649: :Greta gc:sibling :Geert .
[by CE on 648 (@@_g_L579C9)]
650: ...
[by parsing <gedcom-facts.n3>]
651: <http://www.agfa.com/w3c/euler/gedcom-facts#Geert> :sex :Male .
[by CE on 650 (@@_g_L683C9)]
652: ...
[by parsing <gedcom-relations.n3>]
653: @forAll :C, :S . { :C gc:sibling :S . :S gc:sex gc:Male . }
log:implies {:C gc:brother :S . } .
[by CE on 652 (@@_g_L686C16)]
654: :Greta gc:brother :Geert .
[by GMP on 653, [649, 651]]
655: :Greta gc:brother :Geert .
[by CE on 654 (@@_g_L578C7)]
656: ...
[by parsing <gedcom-relations.n3>]
657: @forAll :C, :P, :U . { :C gc:parent :P . :P gc:brother :U . }
log:implies {:C gc:uncle :U . } .
[by CE on 656 (@@_g_L690C14)]
658: :Tom gc:uncle :Geert .
[by GMP on 657, [555, 655]]
659: :Tom gc:uncle :Geert .
[by CE on 658 (@@_g_L570C5)]
660: ...
[by parsing <gedcom-filter.n3>]
661: @forAll :A, :D, :M, :S . { :A gc:mother :M . :D gc:son :S . :M
gc:daughter :D . :S gc:uncle :A . } log:implies {:A
<http://www.agfa.com/w3c/euler/gedcom-facts#testRelationship> :S . } .
[by CE on 660 (@@_g_L695C12)]
662: :Geert :testRelationship :Tom .
[by GMP on 661, [519, 533, 547, 659]]
663: ...
[by parsing <gedcom-facts.n3>]
664: :Jos gc:childIn :dp .
[by CE on 663 (@@_g_L699C9)]
665: ...
[by parsing <gedcom-facts.n3>]
666: :Maria gc:spouseIn :dp .
[by CE on 665 (@@_g_L700C9)]
667: ...
[by parsing <gedcom-relations.n3>]
668: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 667 (@@_g_L704C16)]
669: :Jos gc:parent :Maria .
[by GMP on 668, [664, 666]]
670: :Jos gc:parent :Maria .
[by CE on 669 (@@_g_L698C7)]
671: ...
[by parsing <gedcom-facts.n3>]
672: <http://www.agfa.com/w3c/euler/gedcom-facts#Maria> :sex :Female .
[by CE on 671 (@@_g_L705C7)]
673: ...
[by parsing <gedcom-relations.n3>]
674: @forAll :C, :P . { :C gc:parent :P . :P gc:sex gc:Female . }
log:implies {:C gc:mother :P . } .
[by CE on 673 (@@_g_L708C14)]
675: :Jos gc:mother :Maria .
[by GMP on 674, [670, 672]]
676: :Jos gc:mother :Maria .
[by CE on 675 (@@_g_L697C5)]
677: ...
[by parsing <gedcom-facts.n3>]
678: :Greta gc:childIn :dp .
[by CE on 677 (@@_g_L711C9)]
679: ...
[by parsing <gedcom-facts.n3>]
680: :Maria gc:spouseIn :dp .
[by CE on 679 (@@_g_L712C9)]
681: ...
[by parsing <gedcom-relations.n3>]
682: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 681 (@@_g_L716C16)]
683: :Greta gc:parent :Maria .
[by GMP on 682, [678, 680]]
684: :Greta gc:parent :Maria .
[by CE on 683 (@@_g_L710C7)]
685: ...
[by parsing <gedcom-facts.n3>]
686: <http://www.agfa.com/w3c/euler/gedcom-facts#Greta> :sex :Female .
[by CE on 685 (@@_g_L717C7)]
687: ...
[by parsing <gedcom-relations.n3>]
688: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Female . } log:implies
{:P gc:daughter :C . } .
[by CE on 687 (@@_g_L720C14)]
689: :Maria gc:daughter :Greta .
[by GMP on 688, [684, 686]]
690: :Maria gc:daughter :Greta .
[by CE on 689 (@@_g_L709C5)]
691: ...
[by parsing <gedcom-facts.n3>]
692: :Tom gc:childIn :sd .
[by CE on 691 (@@_g_L723C9)]
693: ...
[by parsing <gedcom-facts.n3>]
694: :Greta gc:spouseIn :sd .
[by CE on 693 (@@_g_L724C9)]
695: ...
[by parsing <gedcom-relations.n3>]
696: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 695 (@@_g_L728C16)]
697: :Tom gc:parent :Greta .
[by GMP on 696, [692, 694]]
698: :Tom gc:parent :Greta .
[by CE on 697 (@@_g_L722C7)]
699: ...
[by parsing <gedcom-facts.n3>]
700: <http://www.agfa.com/w3c/euler/gedcom-facts#Tom> :sex :Male .
[by CE on 699 (@@_g_L729C7)]
701: ...
[by parsing <gedcom-relations.n3>]
702: @forAll :C, :P . { :C gc:parent :P; gc:sex gc:Male . } log:implies
{:P gc:son :C . } .
[by CE on 701 (@@_g_L732C14)]
703: :Greta gc:son :Tom .
[by GMP on 702, [698, 700]]
704: :Greta gc:son :Tom .
[by CE on 703 (@@_g_L721C5)]
705: ...
[by parsing <gedcom-facts.n3>]
706: :Tom gc:childIn :sd .
[by CE on 705 (@@_g_L735C9)]
707: ...
[by parsing <gedcom-facts.n3>]
708: :Greta gc:spouseIn :sd .
[by CE on 707 (@@_g_L736C9)]
709: ...
[by parsing <gedcom-relations.n3>]
710: @forAll :C, :F, :P . { :C gc:childIn :F . :P gc:spouseIn :F . }
log:implies {:C gc:parent :P . } .
[by CE on 709 (@@_g_L740C16)]
711: :Tom gc:parent :Greta .
[by GMP on 710, [706, 708]]
712: :Tom gc:parent :Greta .
[by CE on 711 (@@_g_L734C7)]
713: ...
[by parsing <gedcom-relations.n3>]
714: :sibling a owl:SymmetricProperty .
[by CE on 713 (@@_g_L743C11)]
715: ...
[by parsing <gedcom-facts.n3>]
716: :Jos gc:childIn :dp .
[by CE on 715 (@@_g_L745C13)]
717: ...
[by parsing <gedcom-facts.n3>]
718: :Greta gc:childIn :dp .
[by CE on 717 (@@_g_L746C13)]
719: ...
[by parsing <gedcom-facts.n3>]
720: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 719 (@@_g_L748C15)]
721: ...
[by parsing <rpo-rules.n3>]
722: owl:distinctMembers :range rdf:List .
[by CE on 721 (@@_g_L751C19)]
723: ...
[by parsing <gedcom-facts.n3>]
724: :dp owl:distinctMembers ( :Jos :Rita :Geert :Caroline :Dirk :Greta )
.
[by CE on 723 (@@_g_L752C19)]
725: ...
[by parsing <rpo-rules.n3>]
726: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 725 (@@_g_L757C26)]
727: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 726, [722, 724]]
728: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 727 (@@_g_L750C17)]
729: ...
[by parsing <rpo-rules.n3>]
730: @forAll :L . { :L a rdf:List . } log:implies {:L p0:subListOf :L . }
.
[by CE on 729 (@@_g_L759C24)]
731: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos
:Rita :Geert :Caroline :Dirk :Greta ) .
[by GMP on 730, [728]]
732: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) p0:subListOf ( :Jos
:Rita :Geert :Caroline :Dirk :Greta ) .
[by CE on 731 (@@_g_L749C15)]
733: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:first]
734: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
735: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
736: ...
[by parsing <rpo-rules.n3>]
737: rdf:rest :range rdf:List .
[by CE on 736 (@@_g_L765C19)]
738: ( :Jos :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
739: ...
[by parsing <rpo-rules.n3>]
740: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 739 (@@_g_L771C26)]
741: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 740, [737, 738]]
742: ( :Rita :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 741 (@@_g_L764C17)]
743: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
744: ...
[by parsing <rpo-rules.n3>]
745: rdf:rest :range rdf:List .
[by CE on 744 (@@_g_L775C21)]
746: ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
747: ...
[by parsing <rpo-rules.n3>]
748: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 747 (@@_g_L781C28)]
749: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 748, [745, 746]]
750: ( :Geert :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 749 (@@_g_L774C19)]
751: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
752: ...
[by parsing <rpo-rules.n3>]
753: rdf:rest :range rdf:List .
[by CE on 752 (@@_g_L785C23)]
754: ( :Geert :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
755: ...
[by parsing <rpo-rules.n3>]
756: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 755 (@@_g_L791C30)]
757: ( :Caroline :Dirk :Greta ) a rdf:List .
[by GMP on 756, [753, 754]]
758: ( :Caroline :Dirk :Greta ) a rdf:List .
[by CE on 757 (@@_g_L784C21)]
759: ( :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
760: ...
[by parsing <rpo-rules.n3>]
761: rdf:rest :range rdf:List .
[by CE on 760 (@@_g_L795C25)]
762: ( :Caroline :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
763: ...
[by parsing <rpo-rules.n3>]
764: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 763 (@@_g_L801C32)]
765: ( :Dirk :Greta ) a rdf:List .
[by GMP on 764, [761, 762]]
766: ( :Dirk :Greta ) a rdf:List .
[by CE on 765 (@@_g_L794C23)]
767: ( :Greta ) .
[by built-in Axiom rdf:first]
768: ...
[by parsing <rpo-rules.n3>]
769: rdf:rest :range rdf:List .
[by CE on 768 (@@_g_L805C27)]
770: ( :Dirk :Greta ) .
[by built-in Axiom rdf:rest]
771: ...
[by parsing <rpo-rules.n3>]
772: @forAll :C, :O, :P, :S . { :P rdfs:range :C . :S :P :O . }
log:implies {:O a :C . } .
[by CE on 771 (@@_g_L811C34)]
773: ( :Greta ) a rdf:List .
[by GMP on 772, [769, 770]]
774: ( :Greta ) a rdf:List .
[by CE on 773 (@@_g_L804C25)]
775: ...
[by parsing <rpo-rules.n3>]
776: @forAll :I, :L . { :L a rdf:List; rdf:first :I . } log:implies {:I
list:in :L . } .
[by CE on 775 (@@_g_L814C32)]
777: :Greta list:in ( :Greta ) .
[by GMP on 776, [767, 774]]
778: :Greta list:in ( :Greta ) .
[by CE on 777 (@@_g_L802C23)]
779: ...
[by parsing <rpo-rules.n3>]
780: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 779 (@@_g_L818C30)]
781: :Greta list:in ( :Dirk :Greta ) .
[by GMP on 780, [759, 766, 778]]
782: :Greta list:in ( :Dirk :Greta ) .
[by CE on 781 (@@_g_L792C21)]
783: ...
[by parsing <rpo-rules.n3>]
784: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 783 (@@_g_L822C28)]
785: :Greta list:in ( :Caroline :Dirk :Greta ) .
[by GMP on 784, [751, 758, 782]]
786: :Greta list:in ( :Caroline :Dirk :Greta ) .
[by CE on 785 (@@_g_L782C19)]
787: ...
[by parsing <rpo-rules.n3>]
788: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 787 (@@_g_L826C26)]
789: :Greta list:in ( :Geert :Caroline :Dirk :Greta ) .
[by GMP on 788, [743, 750, 786]]
790: :Greta list:in ( :Geert :Caroline :Dirk :Greta ) .
[by CE on 789 (@@_g_L772C17)]
791: ...
[by parsing <rpo-rules.n3>]
792: @forAll :I, :L, :R . { :I list:in :R . :L a rdf:List; rdf:rest :R . }
log:implies {:I list:in :L . } .
[by CE on 791 (@@_g_L830C24)]
793: :Greta list:in ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by GMP on 792, [735, 742, 790]]
794: :Greta list:in ( :Rita :Geert :Caroline :Dirk :Greta ) .
[by CE on 793 (@@_g_L762C15)]
795: ...
[by parsing <rpo-rules.n3>]
796: @forAll :A, :D, :L, :R, :X, :Y . { :A owl:distinctMembers :D . :L
p0:subListOf :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies
{:X owl:differentFrom :Y . } .
[by CE on 795 (@@_g_L837C22)]
797: :Jos owl:differentFrom :Greta .
[by GMP on 796, [720, 732, 733, 734, 794]]
798: :Jos owl:differentFrom :Greta .
[by CE on 797 (@@_g_L747C13)]
799: ...
[by parsing <gedcom-relations.n3>]
800: @forAll :C, :C2, :F . { :C gc:childIn :F; owl:differentFrom :C2 . :C2
gc:childIn :F . } log:implies {:C gc:sibling :C2 . } .
[by CE on 799 (@@_g_L841C20)]
801: :Jos gc:sibling :Greta .
[by GMP on 800, [716, 718, 798]]
802: :Jos gc:sibling :Greta .
[by CE on 801 (@@_g_L744C11)]
803: ...
[by parsing <rpo-rules.n3>]
804: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . }
log:implies {:O :P :S . } .
[by CE on 803 (@@_g_L845C18)]
805: :Greta gc:sibling :Jos .
[by GMP on 804, [714, 802]]
806: :Greta gc:sibling :Jos .
[by CE on 805 (@@_g_L742C9)]
807: ...
[by parsing <gedcom-facts.n3>]
808: <http://www.agfa.com/w3c/euler/gedcom-facts#Jos> :sex :Male .
[by CE on 807 (@@_g_L846C9)]
809: ...
[by parsing <gedcom-relations.n3>]
810: @forAll :C, :S . { :C gc:sibling :S . :S gc:sex gc:Male . }
log:implies {:C gc:brother :S . } .
[by CE on 809 (@@_g_L849C16)]
811: :Greta gc:brother :Jos .
[by GMP on 810, [806, 808]]
812: :Greta gc:brother :Jos .
[by CE on 811 (@@_g_L741C7)]
813: ...
[by parsing <gedcom-relations.n3>]
814: @forAll :C, :P, :U . { :C gc:parent :P . :P gc:brother :U . }
log:implies {:C gc:uncle :U . } .
[by CE on 813 (@@_g_L853C14)]
815: :Tom gc:uncle :Jos .
[by GMP on 814, [712, 812]]
816: :Tom gc:uncle :Jos .
[by CE on 815 (@@_g_L733C5)]
817: ...
[by parsing <gedcom-filter.n3>]
818: @forAll :A, :D, :M, :S . { :A gc:mother :M . :D gc:son :S . :M
gc:daughter :D . :S gc:uncle :A . } log:implies {:A
<http://www.agfa.com/w3c/euler/gedcom-facts#testRelationship> :S . } .
[by CE on 817 (@@_g_L858C12)]
819: :Jos :testRelationship :Tom .
[by GMP on 818, [676, 690, 704, 816]]
820: :Dirk :testRelationship :Bart, :Tom . :Geert :testRelationship :Bart,
:Tom . :Jos :testRelationship :Bart, :Tom .
[by CI on [109, 224, 363, 505, 662, 819]]
--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Friday, 8 September 2006 11:47:18 UTC