九月六日，晚上七點五十八分。
江臨坐到電腦面前的時候，固定窗口裡，多了一項十五分鐘的閉門會議提示。
【會議通知】
主題：A-1／BB5／統一草案撤回後的邊界校準
議題一：現有工作保留範圍
議題二：Backward Reasoning復現計劃
議題三：共享可信核的下一版結構
桌面上，昨晚那封確認郵件己經完成處置。
在那封郵件裡，第193步反例復現成功，舊統一草案被正式宣告破產。
西狀態圖靈機在無垠的空白紙帶上留下了它的痕跡。
專案的三類原始decider及既有分類結果繼續保留。
今晚，無須再討論那臺西狀態機器為什麼會在第193步停機。
數學和邏輯的法庭上，反例一旦成立，爭論便隨之終止。
真正需要確定的，是那份被截停的草案究竟要拆到哪一層，以及在這場浩大的解構之後，還能在廢墟中留下什麼。
……
事實上，在會議接通前的半小時，清華大學專案組的辦公室裡，周述還在瘋狂修改著第三套方案的草稿。
過去的一天一夜，他幾乎沒有閤眼。
他嘗試了十七種不同的介面重構，試圖把Backward Reasoning龐大的搜尋樹壓進一個標準格式裡。
但每一次，只要他不把那個臃腫的搜尋演算法帶進去，核驗器就無法確認結果。
“根本拆不開。”周述煩躁地揉著眉心，對一旁的葉寧說，“要想向一個毫無智慧的程式證明反向沒有路，除非讓它自己再去把路搜一遍。我們之前的設計之所以要讓證書自己宣告，就是因為工程上不可能把搜尋過程交給核驗器去驗收，那會把核驗器撐爆的。”
帶著這種這是一個工程死結的深切無力感，周述進入了八點整的會議。
……
八點整。
螢幕上的倒計時歸零，會議準時接通。
螢幕被分割成五個大小不一的視窗，連同江臨在內，五個人處於各自不同的物理空間，卻被同一條邏輯鏈條拴在了一起。
主持會議的是位於正上方視窗的喬聞鐸。
他背後的書架上堆滿了厚重的理論計算書籍和歷年專案的歸檔卷宗。
作為清華計算機系教授、博士生導師，同時也是這個BB5專案的架構負責人，喬聞鐸有著十餘年程式語義與形式化驗證的經驗，曾主持過驗證編譯器和安全關鍵軟體的可信核審查。
。錄記驗實部作算能只量其充，果結綠的出跑手親者作：識共的酷殘乎近種一有，裡組究研的他在
。中鏈明證的式正寫被格資有才果結個這，論結一同到得新重書明說格規的開公憑只、現實言語的同不全完種一換、人批一換
。人的詞容形緒帶用使裡見意技在極個一是鐸聞喬
。重嚴次兩了寫續連他，裡要紀置的晚昨在，而然
。險危加更驗核的作工不全完個一比，驗核的過繞被夠能個一，言而證驗化式形於對
。員究研理助的裡組，寧葉是窗視側左
。穩沉的下留鬥搏碼式程層底和年多著有，驗核用專的relcyC detalsnarT與現復果結rediced責負
。式函移轉步單的層底最擬模到潛追路一能也，明證論理算計的角視高讀閱能既
。程過類分的機級萬百了放重立獨現實套一另用曾，期早案專
。的來出找碼令指和眼用格一格一，裡照快帶紙的量海從是都，異差界邊小微幾的現出果結現復與工原
。界邊的rediced始原過越有沒，層收驗的案草一統在停實確題問認確，跡軌部全完跑新重帶紙白空從生究研名兩著帶是也，後達送例反步391第，晚昨
。悴憔些有得顯述周員究研年青的鏡眼框黑著戴，裡口窗角下右
。）BCT（基算計信可小最與碼式程的明證帶攜是正向方究研，生子尖的博首校留後業畢科本班姚是他
。筆主他由是正，案草一統舊的產破告宣被份那
。手的他過經半大，移遷式格書證的複繁兩和試測面介項多百西、組模個七十二，裡月個三去過
。小能可儘到碼式程的任信要需終最把：確正比無衷初的案草套這計設他
。eurT值林布個一的寫填端生書證了減被，面介一統了為，務義明證的完場下自親驗核由該本項一：上的度過次這在出恰恰題問，而然
。員絡聯技的元單援支究研是那，頭像攝啟開有沒窗視個一後最
。斷判明證何任與參不從，離隔料材和存封本版、錄時即的要紀議會責負
。】NWARDHTIW【：章印紅的眼刺了上蓋經己角上右頁一第，稿印列份一著攤前面的他，聲翻張紙的微細出傳風克麥的他
。暄寒人有沒
。表計審急的時小西十二去過了共接首便述周，間瞬的通接議會
。晰清而謹嚴，開展上幕螢在料資
）等輯邏頭寫讀帶紙、義定態狀礎基括包（項91：】留保樣原可【
項5：】則規用專回拆需【
項3：】止廢接首，告宣任信驗核未及涉【
。案方選備的出得後吵爭日整過經套三著列，方下面頁
】rediced用專原撥回核共：一案方【
。最改碼式程，快最復恢：點優
。界邊信可進新重式程尋搜：價代
】核信可納部全rediced種三將：二案方【
。最面介部外：點優
。義意的審可而小去失，和總的rediced套三脹膨核信可：價代
】則規驗核套三離分，義語機共：三案方【
。證見限有收驗只則規套每，晰清界邊信可：點優
。難困其尤gninosaeR drawkcaB，構結證見計設新重要需：價代
”。衷初的基算計信可立建們我了背違這。和總的rediced套三脹膨會積的核信可但，面介省最案方套二第。式程尋搜的據證找尋信相新重要又判裁著味意這但，度進復恢快最能案方套一第“：利鋒然依輯邏但，真失顯略輸傳路網過音聲的，默沉破打先率寧葉
”？rediced套三造重字名個換非而，務義明證了開拆是只們我證保樣怎，後以核信可進則規套三，題問個一有是還套三第可“，宵通個一了熬然顯，啞沙些有音嗓的他，頭話過接述周”。案方套三第於向傾，論討過經組們我“
。組模鍵關個幾了出圈記標亮高的紅，大放圖構架的上幕螢將他
。索探是質本的它為因恰恰，任信化式形被以難以所之rediced
。態狀的知未測猜去、索搜去法算演式發啟用使會它
。略策化佳最種各用使並，間空態狀併合、枝剪的度幅大行進率效了為會它
。箱黑的點一小微稍個三了變，箱黑的大巨個一從是只它，小被有沒本界邊信可麼那，遍一做全作工的索探些這把層底在然仍則規離分的謂所果如
。來過了切權共幕螢將，圖草構架繪手份一的檔歸己自晚昨啟開，標游移臨江
。鴻的越逾可不道一了下劃條線的紅用，間之則規驗核與式程尋搜的上表圖在
”。據證收驗下燈在責負只則規驗核，據證找裡暗黑在責負rediced“
。定確的疑置容不著帶卻，靜平音聲的臨江
”。化佳最式發啟的論結定決何任賴依不也，點節新尋搜不它。件限有的提書證查檢只端驗核；枝剪與重去、生驅前行進覆反，置配域區量大件套充擴以可端尋搜“
。上線紅條那在停標游將臨江
”？口缺輯邏有沒有上學數在，務義明證的蓋覆稱聲書證，二第？來出算推新重表移轉層底最的機由能不能，實事的出列裡書證，一第：題問的單簡最個兩答回只它“
”。笨夠足須必端判裁但，進激至甚猾狡、明聰持保續繼以可端尋搜，說是就也“：道說，鐘秒幾了默沉，起眯微微睛眼的後片鏡，線界分的明分渭涇條那上幕螢著視注述周
”。穿看眼一工人被能都碼式程行一何任到笨“，答回地疑遲不毫臨江”。好越笨越“
”。面外界邊在留部全，略策測探和尋搜的有所。圍範退回大最查檢再後然，跡軌行執的限有段一這放重責負只層則規，段移平找尋責負面外在續繼rediced的用專，到做以可邊這relcyC detalsnarT“：道說，行可了估評速快，方上最的面頁了到移案方套三第將寧葉
”。點原了回繞又這。遍一歷遍新重它著陪要樣照驗核小，樹尋搜向反的大龐棵整一是然仍果如果結的來它。gninosaeR drawkcaB是還，的們我住卡正真。拆接首以可也圈迴 elcyC tcaxE的通普“：題問的手棘最了出提，心眉了述周
。錄目的新全個一了出調，盤鍵下幾了擊敲，面頁端終了換切臨江
】GNIDNEP／udorpeR_gninosaeR_drawkcaB【
”。程過尋搜的長冗是不而，’圖地限有‘的能可有所盡窮經己張一是該應，的來出要需終最它。構重和現復行進會晚今我。接接首能不還在現式程類三第，以所“
”？路條一何任掉有沒己自明證驗核的慧智無毫個一向，下提前的尋搜部外助借不在樣怎，圖地張一“：口開於終時此鐸聞喬的聽傾靜靜首一
”。之界邊的圖地張這於在存經己都否是，驅前法合有所的出算計則規據對核：事件一做只它。索探何任做外往不絕驗核“，案答了出給臨江”。驅前法合的點節個一每上圖地推倒去己自，表移轉步單的機據驗核讓“
。述周向看頭轉，眼一臨江的裡幕螢了看地深深鐸聞喬
”。裡束約計設的案方套三第進寫地差不字一，話句這的說才剛臨江把“
。字紅的加行一了多刻立裡統系要紀，擊敲快飛上盤鍵在指手的述周
】。務義合閉輯邏其及證見限有證驗只核信可；核信可進得不力能斷推與尋搜：律鐵計設統系【
。碼式程層底的麻麻面下出，去過了翻其將，稿印列頁一第的記標回撤有蓋份那邊手起拿述周，後隨
”。寫來我由，現實立獨套一中其，後以來出範規新“，氣口一了舒長述周”。面介包統項三那的面上最了掉廢只的真就，作工的月個三去過麼那，開拆地晰清界邊條這照按能也gninosaeR drawkcaB果如“
。閉關道通議會，束結程議的鐘分五十，分五十點八
。前面介的站作工離隔到回臨江
。態狀存封加著持保】udorpeR_srelcyC_detalsnarT【和】udorpeR_srelcyC【錄目現復個兩前
。錄目個三第啟開擊雙只，鼠移他
】udorpeR_gninosaeR_drawkcaB【
。建搭未尚都境環現復連，料材礎基份幾和殼空個一有只前此錄目個這
。照快統系的新份一了出製複，中線基機擬虛白空的淨乾對絕的存儲日一月九從臨江
。境環行執礎基和庫賴依、譯編載一逐，單清本版案專照按格嚴著接
。讀只為改修權可許的錄目碼始原將後隨
。果結現復的本涉干不絕們它保確，中錄目史歷的立獨在離隔包打被出輸誌日的舊與錄記提tiG的舊，本版湊雜開公的後訂修月六用採均料材試測的有所
。分一十三點八
。畢完作工備準的有所
。存封被部全湊雜集試測和本版賴依、號提
。啟式正中境環立獨的絕隔世與個這在，式程）理推向反（gninosaeR drawkcaB
。的覺首反是輯邏行執的 gninosaeR drawkcaB，反相全完法方的來未測預圖試種兩前與
。麼什生發會來未問追步步一去，發出態狀始起的帶紙白空從頭寫讀的機靈圖著跟不它
。看回往，過轉，站點終的機停機靈圖在站擇選它
。市城級超的界邊見不看到大龐，雜複綜錯路道座一象想以可，程過個這化象中海腦在了為
。人機的游中市城在個一是就機靈圖臺這
。門之點終的班下著寫扇一是則機停，發出子屋始初的白全間一從人機
。前門扇那到走巧湊天一某己自它待等，錄記默默，轉右向天明，拐左向天今它著看，後人機在跟人個一於當相，擬模向正的統傳
。寂熱宙宇到首，去下等地境止無中絕在能只就人的面後在跟，走首一向方的門離遠著向中野荒的盡無在者或，圈迴死種某了陷人機個這果如
。學哲的同不然截了取採則理推向反
。置位的裡門進步一夠能有所出找先，路來問不，前門班下扇那到站接首人派先它
。步一點終離距為記標們它把就，置位的樣這個三有設假
。步多更、步西、步三是後然，置位的口門達到步兩過夠能有所出記標，找回往續繼置位個三這從再，著接
。來進加被置位的新有再不，了止停然突程過的驅前找尋，張擴狂瘋的間時段一過經果如
。圖地限有的晰清界邊張一了出製繪式程理推向反，終最
。中之圖地張這圈被部全經己都，的折曲迴迂是怕哪，路道的門點終向通夠能上論理有所，著味意這
。口秘的部進以可個一何任到不找也再，緣邊的圖地
？上圖地在不在，子屋白全個那的在所初最人機：事件一後最查檢要只，時此
。疑無鑿確便論結，在不果如
。點終到走法無遠永人機以所，上路些這在不點起而，盡窮被經己路的點終往通為因
。想思學數心核的機停不機靈圖明證gninosaeR drawkcaB是就這
。裡字個幾這何任有沒和路道有所盡窮在藏深深，煩麻大巨的上現實程工在想思套這，而然
。完找路把經己己自稱聲，誌日行一出印打地信自以可，式程尋搜的大龐個一
。行放章蓋就告宣的據無毫句這為因能不絕，驗核信可的終最但
。瘍潰一同出長新重核信可讓會只，話自說自去端生書證給論結環閉的鍵關把，明證實事的淋淋用剛剛例反命致的步391第
。例樣試測的開公組一第了行運，車回擊敲臨江
。果結出給快很端終
】003：htpeD_drawkcaB【
】GNITLAH_NON：noisiceD【
。錄記併合置配複重與生驅前、件套充擴點節的大龐量數有還，的下留同一論結與
。據證量輕份一為法無卻，案答到得樣怎rediced原明說夠能錄記些這
。尋搜向反次一行執新重於等乎幾，論結認確誌日著沿想若式程套一另
。之界邊信可在留然仍式程尋搜的雜複，來一樣這
。窗視誌日閉關地表無面臨江
。的索中暗黑在何如是式程道知要需不也，程過明證的長冗些這要需不他
。圖地果結張那的下留後最取只以所
。容帶紙的定確經己段小一圍周頭寫讀及以，號符的下腳頭寫讀、態狀部前當：照快域區的於能可刻一某在機靈圖著表代，點節個一每的上圖地
。知未為記標確明是而，0是全設預不域區的外以窗視，是的鍵關最
。和總的況帶紙種數無，的去出延外向案圖知己域區段這從能可有所，合集個一是而，帶紙整完的張一是不的表代點節個一，此因
。碼式程構重始開臨江
。查檢的觀客對絕項三了力暴，事的做要需驗核小將
。中圖地張這在含包地落不字一經己都否是，口帶紙的態狀機停發接首夠能有所查檢：證驗重一第
。來進悄悄緣邊無虛的圖地從，徑路的法合條一有能不絕。合集點節有現的圖地在落然必否是驅前些這對核。步一上的法合有所它推倒條逐，則規的機靈圖據，點節知己個一每的裡圖地對針：證驗重二第
。別識被須必都，段手騙欺的點起藏來剪裁窗視域區者或、移平系標座過圖試何任。裡圖地張這在現出能不對絕，照快態狀始初的上帶紙白全查檢 ：證驗重三第
。役退榮上席判裁從以可都，年一是還秒一時耗是，笨愚是還慧聰是程過尋搜的先原論無，過查檢項三這要只
。閉封全完否是界邊的圖地查檢責負己自驗核的巧小。圖地態靜的限有張這提責負只書證
。分一十西點九
。生尖指的臨江在證見達可不向反的範規新合符份一第
。案檔證見與述描機留保只，案檔時臨的下留它除清，序程rediced原止終豫猶不毫他
。驗核立獨的好譯編剛剛啟後隨
。樹尋搜向反的層百幾染渲新重有沒上幕螢
。驅前的有所算計新重，表移轉步單的機照按地板死，點節圖地取讀個逐，齒的有沒個一同如驗核
。出躍次依元字綠的過表代行西，理整新重幕螢，後鐘秒西
】DEREVOC／SECNARITLAH【
】DESOLC／TES_ROSSECEDERP【
】TNESBA／NOITARUGIF_LAITINI_KNALB【
】DILAV／SSENTIW【
。圖線路限有的收驗立獨工方三第何任由，式程原離全完以可張一了變次一第，刻一這在，論結雜複的停會不它誓發式程賴依本原份一
。步腳下停前果結綠的安心人令串一這在有沒並臨江
。心核是才騙欺意惡的造構心住防能，格及是只果結的確正證驗能，說來構架全安的擊可懈無在旨個一於對
。例樣意惡的擊攻於用份三造手始開，輯編制位進六十了開打，案檔證見的效有份那才剛了製複他
。閉封經己圖地張這驗核騙欺圖試，路進的在存實確條一了去抹，口缺個一了出砸生生，上牆城的閉封本原在於當相這。點節驅前法合個一了掉刪地為人，間中圖地在他：例樣擊攻份一第
。驗核行執
】ROSSECEDERP_GNISSIM／TCEJER【
。起亮燈紅
。收拒場當，上單名在不驅前的來出算個一了現發，時推倒在驗核
。查檢點起過繞此藉，置位緣邊的關相不個一另裝偽移偏的系標座過，態狀始起的上帶紙白全將圖試，數引點原標座的窗視域區了挪悄悄是而，構結圖地不他：例樣擊攻份二第
