diff --git a/src/problem.rs b/src/problem.rs
index 9f038aa..6b8e4a7 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -369,171 +369,6 @@ impl Problem
 		Ok(())
 	}
 
-	fn display(&self, output_format: crate::output::Format)
-	{
-		let format_context = FormatContext
-		{
-			program_variable_declaration_ids:
-				std::cell::RefCell::new(VariableDeclarationIDs::new()),
-			integer_variable_declaration_ids:
-				std::cell::RefCell::new(VariableDeclarationIDs::new()),
-			input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(),
-			variable_declaration_domains: &self.variable_declaration_domains.borrow(),
-		};
-
-		let print_title = |title, section_separator|
-		{
-			print!("{}{}", section_separator, "%".repeat(72));
-			print!("\n% {}", title);
-			println!("\n{}", "%".repeat(72));
-		};
-
-		let print_formula = |formula: &foliage::Formula|
-		{
-			match output_format
-			{
-				crate::output::Format::HumanReadable => print!("{}",
-					foliage::format::display_formula(formula, &format_context)),
-				crate::output::Format::TPTP => print!("{}",
-					crate::output::tptp::display_formula(formula, &format_context)),
-			}
-		};
-
-		let mut section_separator = "";
-
-		if output_format == crate::output::Format::TPTP
-		{
-			print_title("anthem types", section_separator);
-			section_separator = "\n";
-
-			let tptp_preamble_anthem_types
-				= include_str!("output/tptp/preamble_types.tptp").trim_end();
-			println!("{}", tptp_preamble_anthem_types);
-
-			print_title("anthem axioms", section_separator);
-
-			let tptp_preamble_anthem_types
-				= include_str!("output/tptp/preamble_axioms.tptp").trim_end();
-			println!("{}", tptp_preamble_anthem_types);
-
-			if !self.predicate_declarations.borrow().is_empty()
-				|| !self.function_declarations.borrow().is_empty()
-			{
-				print_title("types", section_separator);
-
-				if !self.predicate_declarations.borrow().is_empty()
-				{
-					println!("% predicate types")
-				}
-
-				for predicate_declaration in self.predicate_declarations.borrow().iter()
-				{
-					println!("tff(type, type, {}).",
-						crate::output::tptp::display_predicate_declaration(predicate_declaration));
-				}
-
-				if !self.function_declarations.borrow().is_empty()
-				{
-					println!("% function types")
-				}
-
-				for function_declaration in self.function_declarations.borrow().iter()
-				{
-					println!("tff(type, type, {}).",
-						crate::output::tptp::display_function_declaration(function_declaration,
-							&format_context));
-				}
-			}
-
-			let function_declarations = self.function_declarations.borrow();
-			let symbolic_constants = function_declarations.iter().filter(
-				|x| !self.input_constant_declaration_domains.borrow().contains_key(*x));
-
-			let mut last_symbolic_constant: Option<std::rc::Rc<foliage::FunctionDeclaration>> =
-				None;
-
-			for (i, symbolic_constant) in symbolic_constants.enumerate()
-			{
-				// Order axioms are only necessary with two or more symbolic constants
-				if i == 1
-				{
-					println!("% axioms for order of symbolic constants")
-				}
-
-				if symbolic_constant.arity > 0
-				{
-					// TODO: refactor
-					panic!("unexpected n-ary function declaration");
-				}
-
-				if let Some(last_symbolic_constant) = last_symbolic_constant
-				{
-					println!("tff(symbolic_constant_order, axiom, p__less__({}, {})).",
-						last_symbolic_constant.name, symbolic_constant.name);
-				}
-
-				last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant));
-			}
-		}
-
-		for (section_kind, statements) in self.statements.borrow().iter()
-		{
-			if statements.is_empty()
-			{
-				continue;
-			}
-
-			let title = match section_kind
-			{
-				SectionKind::CompletedDefinitions => "completed definitions",
-				SectionKind::IntegrityConstraints => "integrity constraints",
-				SectionKind::Axioms => "axioms",
-				SectionKind::Assumptions => "assumptions",
-				SectionKind::Lemmas => "lemmas",
-				SectionKind::Assertions => "assertions",
-			};
-
-			print_title(title, section_separator);
-			section_separator = "\n";
-
-			let mut i = 0;
-
-			for statement in statements.iter()
-			{
-				if let Some(ref description) = statement.description
-				{
-					println!("% {}", description);
-				}
-
-				let name = match &statement.name
-				{
-					// TODO: refactor
-					Some(name) => name.clone(),
-					None =>
-					{
-						i += 1;
-						format!("statement_{}", i)
-					},
-				};
-
-				if output_format == crate::output::Format::TPTP
-				{
-					// TODO: add proper statement type
-					print!("tff({}, axiom, ", name);
-				}
-
-				print_formula(&statement.formula);
-
-				if output_format == crate::output::Format::TPTP
-				{
-					print!(").");
-				}
-
-				println!("");
-			}
-		}
-	}
-
 	fn write_tptp_problem_to_prove_next_statement(&self, formatter: &mut String) -> std::fmt::Result
 	{
 		use std::fmt::Write as _;