Proof
Step Formula Justification Bindings
1 ... parsing <time.n3>
2 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> :propertyDisjointWith <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> . erasure from step 1
3 ... parsing <owl2.n3>
4 :propertyDisjointWith a :SymmetricProperty . erasure from step 3
5 ... parsing <owlth.n3>
6 @forAll :p, :v, :w . { :p a owl:SymmetricProperty . :v :p :w . } log:implies {:w :p :v . } . erasure from step 5
7 ... rule from step 6 applied to steps (2, 4) {'p': u'<http://www.w3.org/2002/07/owl#propertyDisjointWith>', 'w': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'v': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>'}
8 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> :propertyDisjointWith <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> . erasure from step 7
9 <http://sw.opencyc.org/2009/04/07/concept/en/perceives> :subPropertyOf <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> . erasure from step 1
10 { <http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } log:includes {<http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . built-in Axiom log:includes
12 [ a <http://sw.opencyc.org/2009/04/07/concept/en/AffixingSignature>; <http://sw.opencyc.org/2009/04/07/concept/en/objectActedOn> <http://example.org/1995/manifesto>; <http://sw.opencyc.org/2009/04/07/concept/en/performer> :Bob ]. erasure from step 11
13 @forAll :DOC, :WHO . { [ a <http://sw.opencyc.org/2009/04/07/concept/en/AffixingSignature>; <http://sw.opencyc.org/2009/04/07/concept/en/objectActedOn> :DOC; <http://sw.opencyc.org/2009/04/07/concept/en/performer> :WHO ]. } log:implies {:DOC c:speaks_for :WHO . } . erasure from step 11
14 ... rule from step 13 applied to steps (12,) {'DOC': u'<http://example.org/1995/manifesto>', 'WHO': u'<badmeta.n3#Bob>', '_g_L40C8': '[...]'}
15 <http://example.org/1995/manifesto> c:speaks_for :Bob . erasure from step 14
16 ... parsing <httpsocial.n3>
17 :information s:subPropertyOf c:says . erasure from step 16
18 { <http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } log:includes {<http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } . built-in Axiom log:includes
19 <http://example.org/1995/manifesto> :uri "http://example.org/1995/manifesto" . built-in Axiom log:uri
20 ( "http://example.org/1995/manifesto" "http://([^/]+)/" ) :search ( "example.org" ) . built-in Axiom str:search
21 <http://example.org/1995/manifesto> :uri "http://example.org/1995/manifesto" . built-in Axiom log:uri
22 ( :Q1 ) list:member :Q1 . built-in Axiom list:member
23 :A1 hs:messageEntity {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . }; ht:statusCodeNumber "200" . :C1 ht:requests ( :Q1 ) . :Q1 ht:absoluteURI "http://example.org/1995/manifesto"; ht:methodName "GET"; ht:resp :A1 . erasure from step 11
24 ... parsing <httpspeech.n3>
25 @forAll hs:E, hs:RES, :A, :CONNECTION, :I, :Q . { hs:RES log:uri :I . :A hs:messageEntity hs:E; ht:statusCodeNumber "200" . :CONNECTION ht:requests [ list:member :Q ] . :Q ht:absoluteURI :I; ht:methodName "GET"; ht:resp :A . } log:implies {:CONNECTION c:says {hs:RES hs:information hs:E . } . } . erasure from step 24
26 ... rule from step 25 applied to steps (21, 22, 23) {'A': u'<badmeta.n3#A1>', 'E': '{2}', 'I': '"http...esto"', 'RES': u'<http://example.org/1995/manifesto>', 'Q': u'<badmeta.n3#Q1>', 'CONNECTION': u'<badmeta.n3#C1>', '_g_L134C29': '?'}
27 :C1 c:says {<http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } . erasure from step 26
28 :C1 ht:connectionAuthority "example.org" . erasure from step 11
29 @forAll :E, :RES, htt:A, htt:CONNECTION, htt:I . { ( htt:I "http://([^/]+)/" ) str:search ( htt:A ) . :RES log:uri htt:I . htt:CONNECTION c:says {:RES :information :E . }; ht:connectionAuthority htt:A . } log:implies {htt:CONNECTION c:controls_spo ( :RES :information :E ) . } . erasure from step 24
30 ... rule from step 29 applied to steps (19, 20, 27, 28) {'I': '"http...esto"', 'A': '"exam....org"', 'CONNECTION': u'<badmeta.n3#C1>', 'E': '{2}', 'RES': u'<http://example.org/1995/manifesto>'}
31 :C1 c:controls_spo ( <http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } ) . erasure from step 30
32 :C1 c:says {<http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } . erasure from step 26
33 ... parsing <speech.n3>
34 @forAll :obj, :pred, :subj, spe:A . { spe:A :controls_spo ( :subj :pred :obj ); :says [ log:includes {:subj :pred :obj . } ] . } log:implies {:subj :pred :obj . } . erasure from step 33
35 ... rule from step 34 applied to steps (18, 31, 32) {'_g_L76C11': '{manifesto hs:information {2}}', 'subj': u'<http://example.org/1995/manifesto>', 'obj': '{2}', 'A': u'<badmeta.n3#C1>', 'pred': u'<httpspeech#information>'}
36 <http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . erasure from step 35
37 ... parsing <rdfs-nice.n3>
38 @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . erasure from step 37
39 ... rule from step 38 applied to steps (17, 36) {'_g_L71C8': u'<httpspeech#information>', 'xxx': u'<http://example.org/1995/manifesto>', 'yyy': '{2}', 'bbb': u'<speech#says>'}
40 <http://example.org/1995/manifesto> c:says {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . erasure from step 39
41 @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . erasure from step 33
42 ... rule from step 41 applied to steps (15, 40) {'A': u'<http://example.org/1995/manifesto>', 's': '{2}', 'B': u'<badmeta.n3#Bob>'}
43 :Bob c:says {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . erasure from step 42
44 @forAll :SOMEONE, :SOURCE, :WORK . { :SOMEONE c:says [ log:includes {:WORK <http://purl.org/dc/elements/1.1/source> :SOURCE . } ] . } log:implies {:SOMEONE <http://sw.opencyc.org/2009/04/07/concept/en/perceives> :WORK . } . erasure from step 11
45 ... rule from step 44 applied to steps (10, 43) {'_g_L48C24': '{2}', 'WORK': u'<http://penguin-house.example/2008/article2>', 'SOMEONE': u'<badmeta.n3#Bob>', 'SOURCE': u'<http://example.org/1995/manifesto>'}
46 :Bob <http://sw.opencyc.org/2009/04/07/concept/en/perceives> <http://penguin-house.example/2008/article2> . erasure from step 45
47 @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . erasure from step 37
48 ... rule from step 47 applied to steps (9, 46) {'_g_L71C8': u'<http://sw.opencyc.org/2009/04/07/concept/en/perceives>', 'xxx': u'<badmeta.n3#Bob>', 'yyy': u'<http://penguin-house.example/2008/article2>', 'bbb': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>'}
49 :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> <http://penguin-house.example/2008/article2> . erasure from step 48
50 "2006-01-23" :lessThan "2008-05-16" . built-in Axiom str:lessThan
51 @forSome :_g22, :_g23 . :_g22 xsd:date "2008-05-16" . :_g23 xsd:date "2006-01-23" . erasure from step 11
52 @forSome :_g22 . <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO> :_g22 . erasure from step 11
53 <http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO> :subPropertyOf <http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf> . erasure from step 1
54 @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . erasure from step 37
55 ... rule from step 54 applied to steps (52, 53) {'_g_L71C8': u'<http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO>', 'xxx': u'<http://penguin-house.example/2008/article2>', 'yyy': '[...]', 'bbb': u'<http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf>'}
56 @forSome :_g22 . <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf> :_g22 . erasure from step 55
57 @forSome :_g23 . bad:Bob <http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath> :_g23 . erasure from step 11
58 <http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath> :subPropertyOf <http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf> . erasure from step 1
59 @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . erasure from step 37
60 ... rule from step 59 applied to steps (57, 58) {'_g_L71C8': u'<http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath>', 'xxx': u'<badmeta.n3#Bob>', 'yyy': '[...]', 'bbb': u'<http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf>'}
61 @forSome :_g23 . bad:Bob <http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf> :_g23 . erasure from step 60
62 @forAll :TMAX, :TMIN, :TOBJ1, :TOBJ2 . { :TMAX str:lessThan :TMIN . :TOBJ1 <http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf> [ xsd:date :TMAX ] . :TOBJ2 <http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf> [ xsd:date :TMIN ] . } log:implies {:TOBJ1 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> :TOBJ2 . } . erasure from step 1
63 ... rule from step 62 applied to steps (50, 51, 56, 61) {'TMIN': '"2008...5-16"', 'TOBJ1': u'<badmeta.n3#Bob>', 'TOBJ2': u'<http://penguin-house.example/2008/article2>', 'TMAX': '"2006...1-23"', '_g_L51C43': '[...]', '_g_L50C37': '[...]'}
64 :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> <http://penguin-house.example/2008/article2> . erasure from step 63
65 @forAll :P, :X, :Y, :Z . { @forSome run:_g20 . run:_g20 owl:propertyDisjointWith :P . :X run:_g20 :Y; :P :Z . } log:implies {:Y owl:differentFrom :Z . } . erasure from step 3
66 ... rule from step 65 applied to steps (8, 49, 64) {'Y': u'<http://penguin-house.example/2008/article2>', 'X': u'<badmeta.n3#Bob>', 'Z': u'<http://penguin-house.example/2008/article2>', '_g_L12C6': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'P': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>'}
67 <http://penguin-house.example/2008/article2> :differentFrom <http://penguin-house.example/2008/article2> . erasure from step 66
69 @forAll :X . { :X owl:differentFrom :X . } log:implies {:X owl:differentFrom :X . } . erasure from step 68
70 ... rule from step 69 applied to steps (67,) {'X': u'<http://penguin-house.example/2008/article2>'}
71 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> :propertyDisjointWith <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> . erasure from step 7
72 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> a :SymmetricProperty . erasure from step 1
73 :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> <http://penguin-house.example/2008/article2> . erasure from step 48
74 @forAll :p, :v, :w . { :p a owl:SymmetricProperty . :v :p :w . } log:implies {:w :p :v . } . erasure from step 5
75 ... rule from step 74 applied to steps (72, 73) {'p': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'w': u'<http://penguin-house.example/2008/article2>', 'v': u'<badmeta.n3#Bob>'}
76 <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> :Bob . erasure from step 75
77 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> a :SymmetricProperty . erasure from step 1
78 :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> <http://penguin-house.example/2008/article2> . erasure from step 63
79 @forAll :p, :v, :w . { :p a owl:SymmetricProperty . :v :p :w . } log:implies {:w :p :v . } . erasure from step 5
80 ... rule from step 79 applied to steps (77, 78) {'p': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>', 'w': u'<http://penguin-house.example/2008/article2>', 'v': u'<badmeta.n3#Bob>'}
81 <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> :Bob . erasure from step 80
82 @forAll :P, :X, :Y, :Z . { @forSome run:_g20 . run:_g20 owl:propertyDisjointWith :P . :X run:_g20 :Y; :P :Z . } log:implies {:Y owl:differentFrom :Z . } . erasure from step 3
83 ... rule from step 82 applied to steps (71, 76, 81) {'Y': u'<badmeta.n3#Bob>', 'X': u'<http://penguin-house.example/2008/article2>', 'Z': u'<badmeta.n3#Bob>', '_g_L12C6': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'P': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>'}
84 :Bob owl:differentFrom :Bob . erasure from step 83
85 @forAll :X . { :X owl:differentFrom :X . } log:implies {:X owl:differentFrom :X . } . erasure from step 68
86 ... rule from step 85 applied to steps (84,) {'X': u'<badmeta.n3#Bob>'}
87 :Bob owl:differentFrom :Bob . <http://penguin-house.example/2008/article2> owl:differentFrom <http://penguin-house.example/2008/article2> . conjoining steps (70, 86)

Conclusion:

```@prefix : <badmeta.n3#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .

:Bob     owl:differentFrom :Bob .

<http://penguin-house.example/2008/article2>     owl:differentFrom <http://penguin-house.example/2008/article2> .
```