Proof
Step Formula Justification Bindings
1 22 :notGreaterThan 24 . built-in Axiom math:notGreaterThan
2 { ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . } log:includes { ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . } . built-in Axiom log:includes
3 ... parsing <refi_ex.n3>
4 :Spreadsheet c:controls_property :payoff_wait . erasure from step 3
5 { :City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } log:includes {:City_Wide_refi :cost 3700 . } . built-in Axiom log:includes
6 :Citi_Wide_brochure c:says {:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . }; c:speaks_for :City_Wide . erasure from step 3
7 ... parsing <speech.n3>
8 @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . erasure from step 7
9 ... rule from step 8 applied to steps (6,) {'A': u'<refi_ex#Citi_Wide_brochure>', 's': '{3}', 'B': u'<refi_ex#City_Wide>'}
10 :City_Wide c:says {:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } . erasure from step 9
11 :City_Wide c:controls_property :cost . erasure from step 3
12 @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . erasure from step 7
13 ... rule from step 12 applied to steps (5, 10, 11) {'A': u'<refi_ex#City_Wide>', 'pred': u'<refi_ex#cost>', 'obj': '"3700"', 'subj': u'<refi_ex#City_Wide_refi>', '_g_L91C13': '{3}'}
14 :City_Wide_refi :cost 3700 . erasure from step 13
15 :Sam_mortgage :balance 200000; :rate 6.125 . erasure from step 3
16 { :Fed :rate 4.5 . } log:includes {:Fed :rate 4.5 . } . built-in Axiom log:includes
17 :WSJ c:controls_property :rate . erasure from step 3
18 :MelissaByPhone c:says { @forSome run:_g12 . ( :Melissa :WSJ ) c:quoting run:_g12 . run:_g12 c:says {:Fed :rate 4.5 . } . }; c:speaks_for :Melissa . erasure from step 3
19 @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . erasure from step 7
20 ... rule from step 19 applied to steps (18,) {'A': u'<refi_ex#MelissaByPhone>', 's': '{2}', 'B': u'<refi_ex#Melissa>'}
21 :Melissa c:says { @forSome run:_g12 . ( :Melissa :WSJ ) c:quoting run:_g12 . run:_g12 c:says {:Fed :rate 4.5 . } . } . erasure from step 20
22 @forAll :A, :B, :s . { :A :says { ( :A :B ) :quoting [ :says :s ] . } . } log:implies {:B :says :s . } . erasure from step 7
23 ... rule from step 22 applied to steps (21,) {'A': u'<refi_ex#Melissa>', 's': '{Fed rate "4.5"}', 'B': u'<refi_ex#WSJ>'}
24 :WSJ c:says {:Fed :rate 4.5 . } . erasure from step 23
25 @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . erasure from step 7
26 ... rule from step 25 applied to steps (16, 17, 24) {'A': u'<refi_ex#WSJ>', 'pred': u'<refi_ex#rate>', 'obj': '"4.5"', 'subj': u'<refi_ex#Fed>', '_g_L91C13': '{Fed rate "4.5"}'}
27 :Fed :rate 4.5 . erasure from step 26
28 { :City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } log:includes {:City_Wide_refi :rate_offset 0.25 . } . built-in Axiom log:includes
29 :City_Wide c:says {:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } . erasure from step 9
30 :City_Wide c:controls_property :rate_offset . erasure from step 3
31 @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . erasure from step 7
32 ... rule from step 31 applied to steps (28, 29, 30) {'A': u'<refi_ex#City_Wide>', 'pred': u'<refi_ex#rate_offset>', 'obj': '"0.25"', 'subj': u'<refi_ex#City_Wide_refi>', '_g_L91C13': '{3}'}
33 :City_Wide_refi :rate_offset 0.25 . erasure from step 32
34 @forAll :M1, :M2 . { :Fed :rate 4.5 . :M1 :balance 200000; :rate 6.125 . :M2 :cost 3700; :rate_offset 0.25 . } log:implies {:Spreadsheet c:says { ( :M1 :M2 ) :payoff_wait 22 . } . } . erasure from step 3
35 ... rule from step 34 applied to steps (14, 15, 27, 33) {'M1': u'<refi_ex#Sam_mortgage>', 'M2': u'<refi_ex#City_Wide_refi>'}
36 :Spreadsheet c:says { ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . } . erasure from step 35
37 @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . erasure from step 7
38 ... rule from step 37 applied to steps (2, 4, 36) {'A': u'<refi_ex#Spreadsheet>', 'pred': u'<refi_ex#payoff_wait>', 'obj': '"22"', 'subj': '?', '_g_L91C13': '{li2 payoff_wait "22"}'}
39 ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . erasure from step 38
40 @forAll <refi_ex.n3#M> . { ( :Sam_mortgage <refi_ex.n3#M> ) :payoff_wait [ math:notGreaterThan 24 ] . } log:implies {<refi_ex.n3#M> a :GoodOffer . } . erasure from step 3
41 ... rule from step 40 applied to steps (1, 39) {'M': u'<refi_ex#City_Wide_refi>', '_g_L147C35': '"22"'}
42 :City_Wide_refi a :GoodOffer . erasure from step 41
43 ... parsing <refi_goal.n3>
44 @forAll :X . { :X a <refi_ex#GoodOffer> . } log:implies {:X a <refi_ex#GoodOffer> . } . erasure from step 43
45 :City_Wide_refi a :GoodOffer . rule from step 44 applied to steps (42,) {'X': u'<refi_ex#City_Wide_refi>'}

Conclusion:

```@prefix : <refi_ex#> .

:City_Wide_refi     a :GoodOffer .
```