W3C home > Mailing lists > Public > www-archive@w3.org > September 2006

proof checking result for http://eulersharp.sourceforge.net/2006/02swap/gedcomE.n3

From: <jos.deroo@agfa.com>
Date: Fri, 8 Sep 2006 13:46:25 +0200
To: www-archive@w3.org
Message-ID: <OF83CC81B9.0EDEA6DC-ONC12571E3.003F9B76-C12571E3.0040A293@agfa.com>

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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Wednesday, 7 November 2012 14:18:00 GMT