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
11	...	parsing <badmeta.n3>
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
68	...	parsing <contradiction.n3>
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> .