Introduction: The Cholangiocarcinoma Ontology (CCAO) is an application ontology developed to describe in a structured and standardized way various findings related to cholangiocarcinoma (CCA). It is currently applied to document research data elements and electronic health records data of patients with, or suspected to suffer from, CCA in Thailand. It covers aspects such as verbal screening, ultrasound screening, and symptoms and diagnosis. To render the CCAO fully compatible with Basic Formal Ontology 2020 (BFO2020), and to allow for reasoning that goes beyond mere classification, we are developing a first-order logic axiomatization using the Common Logic Interchange Format (CLIF). Methods: We use the same subset and style of CLIF as used in BFO2020. It corresponds to full firstorder logic with negation, equality and multi-argument predicates. The CCAO uses all axioms from BFO2020, and is expanded to include CLIF-based axioms for relevant terms from BFO-compatible ontologies such as the Information Artifact Ontology (IAO) and the Ontology for General Medical Science (OGMS) which hitherto are not yet axiomatized. Whereas the BFO2020 axiomatization quantifies over particulars and universals and uses a time-indexed instance-of predicate linking the former to the latter, CCAO also quantifies over concepts. This allows for a formal integration of terms from non-BFO compatible ontologies such as SNOMED-CT by relating variables that stand for particulars also to concepts using a non-time-indexed individual-of predicate. A BFO2020-style CLIF parser was developed which generates various output files listing syntactic and semantic errors or warnings, predicate templates, and vocabulary used. It produces also grounded and ungrounded logical derivations in clausal form (CF), conjunctive normal form (CNF) and Kowalski-rules using standard skolemization. These transformations are used to evaluate and revise CCAO-axioms where needed and serve also as input for a reasoner capable of term expansion, satisfiability testing and model generation. Results: We developed axioms to differentiate intrahepatic CCA from perihilar CCA and distal CCA, for instance: “(forall (p t) (iff (instance-of p ccao-perihilar-cholangiocarcinoma t) (and (individual-of p sctid-cholangiocarcinoma-of-perihilar-bile-duct) (instance-of p ccao-cholangiocarcinoma t) (exists (h) (and (individual-of h uberon-common-hepatic-duct) (overlap p h t))))))”. This axiom generates 5 Kowalski rules, one being (in a Prolog structure): “if([[individual-of,B,sctid-cholangiocarcinoma-ofperihilar-bile-duct],[individual-of,A,uberon-common-hepatic-duct,C],[instance-of,B,ccao- cholangiocarcinoma,C],[overlap,B,A,C]]),then([instance-of,B,ccao-perihilarcholangiocarcinoma,C]))”. Conclusion: Moving from Protégé to CLIF is challenging but allows dealing with time-indexing, negation and quantification over universals, particulars and concepts. The use of a CLIF parser/generator helps considerably. We will use CLIF to develop axiomatization for all terms in CCAO and then generate therefrom a slim-downed version compatible with Protégé. Acknowledgement: We would like to thank Werner Ceusters, MD for valuable suggestions and software development.