TSPC 5_a_history_of

5_a_history_of_qed
Ken Thompson used this QED at Berkeley before he came to Bell Labs, and among the first things he did on arriving was to write a new version for the MIT CTSS system.

arc(r_0005_0003__used, r_0005_0001__Ken_r_0005_0002__Thompson, arg0).
arc(r_0005_0003__used, r_0005_0004__this_r_0005_0005__QED, arg1).
arc(r_0005_0003__used, r_0005_0007__Berkeley, r_0005_0006__at_nim19).
arc(r_0005_0008__before, r_0005_0003__used, scope).
arc(r_0005_0008__before, r_0005_0010__came, restriction).
arc(r_0005_0010__came, r_0005_0001__Ken_r_0005_0002__Thompson, arg0).
arc(r_0005_0010__came, r_0005_0012__Bell_r_0005_0013__Labs, r_0005_0011__to_nim34).
arc(r_0005_0015__and, r_0005_0008__before, conj1).
arc(r_0005_0015__and, r_0005_0024__was, conj2).
arc(r_0005_0017__the_r_0005_0019__things, r_0005_0018__first, attrib51).
arc(r_0005_0021__did, r_0005_0001__Ken_r_0005_0002__Thompson, arg0).
arc(r_0005_0021__did, r_0005_0017__the_r_0005_0019__things, arg1).
arc(r_0005_0021__did, r_0005_0023__arriving, r_0005_0022__on_nim67).
arc(r_0005_0023__arriving, z_000_5_a_history_of_qed_67, arg0).
arc(r_0005_0024__was, r_0005_0017__the_r_0005_0019__things, r_0005_0016__among_clr48).
arc(r_0005_0024__was, r_0005_0025__to_r_0005_0026__write, arg0).
arc(r_0005_0025__to_r_0005_0026__write, r_0005_0027__a_r_0005_0029__version, arg1).
arc(r_0005_0025__to_r_0005_0026__write, r_0005_0031__the_r_0005_0032__MIT_r_0005_0033__CTSS_r_0005_0034__system, r_0005_0030__for_nim88).
arc(r_0005_0025__to_r_0005_0026__write, z_000_5_a_history_of_qed_72, arg0).
arc(r_0005_0027__a_r_0005_0029__version, r_0005_0028__new, attrib80).

fof(formula,axiom,
    ? [R_5_15_AND,R_5_8_BEFORE,R_5_10_CAME,R_5_12_BELL_LABS,R_5_3_USED,R_5_4_THIS_QED,R_5_7_BERKELEY,R_5_24_WAS,R_5_25_TO_WRITE,Z_5_A_HISTORY_OF_QED_72,R_5_27_A_VERSION,R_5_28_NEW,R_5_31_THE_MIT_CTSS_SYSTEM,R_5_21_DID,R_5_1_KEN_THOMPSON,R_5_17_THE_THINGS,R_5_18_FIRST,R_5_23_ARRIVING,Z_5_A_HISTORY_OF_QED_67] :
      ( bell_Labs(R_5_12_BELL_LABS)
      & this_QED(R_5_4_THIS_QED)
      & berkeley(R_5_7_BERKELEY)
      & new(R_5_28_NEW)
      & the_MIT_CTSS_system(R_5_31_THE_MIT_CTSS_SYSTEM)
      & ken_Thompson(R_5_1_KEN_THOMPSON)
      & first(R_5_18_FIRST)
      & and(R_5_15_AND)
      & conj1(R_5_15_AND,R_5_8_BEFORE)
      & before(R_5_8_BEFORE)
      & conj1(R_5_8_BEFORE,R_5_10_CAME)
      & came(R_5_10_CAME,R_5_1_KEN_THOMPSON)
      & to_nim34(R_5_10_CAME,R_5_12_BELL_LABS)
      & conj2(R_5_8_BEFORE,R_5_3_USED)
      & used(R_5_3_USED,R_5_1_KEN_THOMPSON,R_5_4_THIS_QED)
      & at_nim19(R_5_3_USED,R_5_7_BERKELEY)
      & conj2(R_5_15_AND,R_5_24_WAS)
      & was(R_5_24_WAS,R_5_25_TO_WRITE)
      & to_write(R_5_25_TO_WRITE,Z_5_A_HISTORY_OF_QED_72,R_5_27_A_VERSION)
      & a_version(R_5_27_A_VERSION)
      & attrib80(R_5_27_A_VERSION,R_5_28_NEW)
      & for_nim88(R_5_25_TO_WRITE,R_5_31_THE_MIT_CTSS_SYSTEM)
      & among_clr48(R_5_24_WAS,R_5_17_THE_THINGS)
      & the_things(R_5_17_THE_THINGS)
      & attrib51(R_5_17_THE_THINGS,R_5_18_FIRST)
      & did(R_5_21_DID,R_5_1_KEN_THOMPSON,R_5_17_THE_THINGS)
      & on_nim67(R_5_21_DID,R_5_23_ARRIVING)
      & arriving(R_5_23_ARRIVING,Z_5_A_HISTORY_OF_QED_67) ) ).

( (IP-MAT (ILYR (ILYR (NP-SBJ;{KEN} (NPR Ken;{Ken})
                                    (NPR Thompson;{Thompson}))
                      (VBD;__ used;{use})
                      (NP-OB1;{BERKELEY_QED} (D this;{this})
                                             (NPR QED;{QED}))
                      (PP-NIM (P-ROLE at;{at})
                              (NP (NPR Berkeley;{Berkeley})))
                      (PP-SCON (P-CONN before;{before})
                               (IP-ADV (NP-SBJ;{KEN} (PRO he;{he}))
                                       (VBD;__ came;{come})
                                       (PP-NIM (P-ROLE to;{to})
                                               (NP (NPR Bell;{Bell})
                                                   (NPR Labs;{Labs}))))))
                (PUNC ,)
                (CONJP (CONJ and;{and})
                       (ILYR (PP-TPC-CLR (P-ROLE among;{among})
                                         (NP (D the;{the})
                                             (ADJP (ADJ first;{first}))
                                             (NS things;{thing})
                                             (IP-REL (NP-OB1 *T*)
                                                     (NP-SBJ;{KEN} (PRO he;{he}))
                                                     (DOD;_Tn_ did;{do})
                                                     (PP-NIM (P-ROLE on;{on})
                                                             (IP-PPL2 (VAG;__ arriving;{arrive}))))))
                             (BED;_Ipr_ was;{be[among]})
                             (IP-INF-SBJ (TO to;{to})
                                         (VB;__ write;{write})
                                         (NP-OB1;{CTSS_QED} (D a;{a})
                                                            (ADJP (ADJ new;{new}))
                                                            (N version;{version}))
                                         (PP-NIM (P-ROLE for;{for})
                                                 (NP (D the;{the})
                                                     (NPR MIT;{MIT})
                                                     (NPR CTSS;{CTSS})
                                                     (N system;{system})))))))
          (PUNC .))
  (ID 5_a_history_of_qed))