diff --git a/backend/src/main/kotlin/Main.kt b/backend/src/main/kotlin/Main.kt
index 160a30983..4ec06be53 100644
--- a/backend/src/main/kotlin/Main.kt
+++ b/backend/src/main/kotlin/Main.kt
@@ -32,7 +32,7 @@ val endpoints: Set<Calculus> = setOf<Calculus>(
     NonClausalTableaux(),
     PropositionalSequent(),
     FirstOrderSequent(),
-    SignedModalTableaux()
+    SignedModalTableaux(),
 )
 
 fun main(args: Array<String>) {
@@ -43,7 +43,7 @@ fun main(args: Array<String>) {
     // Verify that no calculus is overriding /admin and /config endpoints
     if (endpoints.any { it.identifier == "admin" || it.identifier == "config" || it.identifier == "stats" }) {
         throw KalkulierbarException(
-            "Set of active calculi contains forbidden identifiers \"admin\", \"config\" or \"stats\""
+            "Set of active calculi contains forbidden identifiers \"admin\", \"config\" or \"stats\"",
         )
     }
     // Pass list of available calculi to StateKeeper
@@ -66,7 +66,6 @@ fun getEnvPort() = System.getenv("PORT")?.toInt() ?: KBAR_DEFAULT_PORT
  */
 @Suppress("ThrowsCount", "MagicNumber", "LongMethod", "ComplexMethod")
 fun httpApi(port: Int, endpoints: Set<Calculus>, listenGlobally: Boolean = false) {
-
     val host = if (listenGlobally) "0.0.0.0" else "localhost"
 
     val app = Javalin.create { config ->
@@ -97,7 +96,7 @@ fun httpApi(port: Int, endpoints: Set<Calculus>, listenGlobally: Boolean = false
                 |
                 |Available calculus endpoints:
                 |${ids.joinToString("\n")}
-            """.trimMargin()
+            """.trimMargin(),
         )
     }
 
@@ -160,7 +159,7 @@ fun createCalculusEndpoints(app: Javalin, calculus: Calculus) {
             """
                 |Calculus "$name" loaded.
                 |Interact via the /parse /move /close and /validate endpoints
-            """.trimMargin()
+            """.trimMargin(),
         )
     }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt b/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt
index a1d188478..2abcddc64 100644
--- a/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt
+++ b/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt
@@ -42,7 +42,7 @@ abstract class ScoredCalculus<State, Move, Param> : JSONCalculus<State, Move, Pa
 
 @Serializable
 data class Scores(
-    val entries: List<Map<String, String>>
+    val entries: List<Map<String, String>>,
 ) {
     val keys = if (entries.isEmpty()) emptyList() else entries[0].keys.toList()
 }
diff --git a/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt b/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt
index 58e653cf1..9b546a5b0 100644
--- a/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt
+++ b/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt
@@ -10,7 +10,10 @@ import kotlinx.serialization.modules.plus
 class DPLL : JSONCalculus<DPLLState, DPLLMove, Unit>() {
     override val identifier = "dpll"
 
-    override val serializer = Json { serializersModule = dpllMoveModule + clausesetDiffModule; encodeDefaults = true }
+    override val serializer = Json {
+        serializersModule = dpllMoveModule + clausesetDiffModule
+        encodeDefaults = true
+    }
     override val moveSerializer = DPLLMove.serializer()
     override val stateSerializer = DPLLState.serializer()
 
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt b/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt
index a402cd24c..bc226fa83 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt
@@ -164,7 +164,7 @@ class Relation(val spelling: String, var arguments: List<FirstOrderTerm>) : Synt
 class UniversalQuantifier(
     override var varName: String,
     override var child: LogicNode,
-    override val boundVariables: MutableList<QuantifiedVariable>
+    override val boundVariables: MutableList<QuantifiedVariable>,
 ) : Quantifier() {
 
     override fun toString() = "(∀$varName: $child)"
@@ -215,7 +215,7 @@ class UniversalQuantifier(
 class ExistentialQuantifier(
     override var varName: String,
     override var child: LogicNode,
-    override val boundVariables: MutableList<QuantifiedVariable>
+    override val boundVariables: MutableList<QuantifiedVariable>,
 ) : Quantifier() {
 
     override fun toString() = "(∃$varName: $child)"
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt
index 411c29024..6bf2ff50a 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt
@@ -55,7 +55,7 @@ class FreeVariableCollector : DoNothingCollector() {
  * @param boundVariables: set of bound variables to compare with variables in first-order term
  */
 class FreeVariableTermCollector(
-    val boundVariables: Set<QuantifiedVariable>
+    val boundVariables: Set<QuantifiedVariable>,
 ) : FirstOrderTermVisitor<Set<QuantifiedVariable>>() {
     override fun visit(node: Constant): Set<QuantifiedVariable> {
         return mutableSetOf()
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt
index 2c46417ad..d85387f26 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt
@@ -53,11 +53,10 @@ class PrenexNormalForm : DoNothingVisitor() {
      * @return quantified sub-formula
      */
     override fun visit(node: UniversalQuantifier): LogicNode {
-
         if (encounteredVars.contains(node.varName)) {
             throw FormulaConversionException(
                 "Prenex Normal Form conversion encountered " +
-                    "double-binding of variable '${node.varName}'"
+                    "double-binding of variable '${node.varName}'",
             )
         }
 
@@ -74,11 +73,10 @@ class PrenexNormalForm : DoNothingVisitor() {
      * @return quantified sub-formula
      */
     override fun visit(node: ExistentialQuantifier): LogicNode {
-
         if (encounteredVars.contains(node.varName)) {
             throw FormulaConversionException(
                 "Prenex Normal Form conversion encountered " +
-                    " double-binding of variable '${node.varName}'"
+                    " double-binding of variable '${node.varName}'",
             )
         }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt
index 1e92f1b25..4fd225cc9 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt
@@ -43,8 +43,10 @@ data class Signature(
     companion object {
         fun empty(): Signature {
             return Signature(
-                constants = setOf(), functions = setOf(),
-                relations = setOf(), boundVariables = setOf()
+                constants = setOf(),
+                functions = setOf(),
+                relations = setOf(),
+                boundVariables = setOf(),
             )
         }
 
@@ -82,7 +84,7 @@ data class Signature(
             constants = constants + sig.constants,
             functions = functions + sig.functions,
             relations = relations + sig.relations,
-            boundVariables = boundVariables + sig.boundVariables
+            boundVariables = boundVariables + sig.boundVariables,
         )
     }
 
@@ -152,7 +154,7 @@ class SignatureExtractor : DoNothingCollector() {
                 constants = instance.constants,
                 functions = instance.functions,
                 relations = instance.relations,
-                boundVariables = instance.boundVariables
+                boundVariables = instance.boundVariables,
             )
         }
     }
@@ -201,7 +203,7 @@ class TermSignatureExtractor(
 
 class SignatureAdherenceChecker(
     private val sig: Signature,
-    private val allowNewConstants: Boolean = true
+    private val allowNewConstants: Boolean = true,
 ) : FirstOrderTermVisitor<Unit>() {
 
     override fun visit(node: Constant) {
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt
index a719f1bc0..f0b7b8813 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt
@@ -63,11 +63,10 @@ class Skolemization(private val signature: Signature) : DoNothingVisitor() {
      * @return Skolemized subformula without the existential quantifier
      */
     override fun visit(node: ExistentialQuantifier): LogicNode {
-
         if (quantifierScope.size > quantifierScope.distinctBy { it.varName }.size) {
             throw FormulaConversionException(
                 "Double-bound universally quantified variable encountered " +
-                    "during Skolemization"
+                    "during Skolemization",
             )
         }
 
@@ -127,7 +126,7 @@ class Skolemization(private val signature: Signature) : DoNothingVisitor() {
  */
 class SkolemTermReplacer(
     private val replacementMap: Map<QuantifiedVariable, FirstOrderTerm>,
-    private val bindingQuantifiers: List<UniversalQuantifier>
+    private val bindingQuantifiers: List<UniversalQuantifier>,
 ) : FirstOrderTermVisitor<FirstOrderTerm>() {
 
     /**
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt
index ff4839fc2..5fbae844f 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt
@@ -8,7 +8,7 @@ import kalkulierbar.logic.QuantifiedVariable
 import kalkulierbar.logic.Quantifier
 
 class VariableInstantiator(
-    private val replacementMap: Map<String, FirstOrderTerm>
+    private val replacementMap: Map<String, FirstOrderTerm>,
 ) : FirstOrderTermVisitor<FirstOrderTerm>() {
 
     companion object {
@@ -172,7 +172,7 @@ class TermContainsVariable(val variable: String) : FirstOrderTermVisitor<Boolean
  */
 class QuantifierLinker(
     private val quantifiers: List<Quantifier>,
-    private val enforceUnique: Boolean
+    private val enforceUnique: Boolean,
 ) : FirstOrderTermVisitor<Unit>() {
 
     /**
@@ -185,12 +185,12 @@ class QuantifierLinker(
         if (matchingQuantifiers.isEmpty()) {
             throw FormulaConversionException(
                 "Error linking variables to quantifiers: " +
-                    "Variable '${node.spelling}' is not bound by any quantifier"
+                    "Variable '${node.spelling}' is not bound by any quantifier",
             )
         } else if (matchingQuantifiers.size > 1 && enforceUnique) {
             throw FormulaConversionException(
                 "Error linking variables to quantifiers: " +
-                    "Variable '${node.spelling}' is bound by more than one quantifier"
+                    "Variable '${node.spelling}' is bound by more than one quantifier",
             )
         }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt
index 00fa19f6d..3648ce26a 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt
@@ -31,8 +31,10 @@ class UniqueVariables : DoNothingVisitor() {
 
     // Keep track of variable version numbers already used
     private val variableDisambCounter = mutableMapOf<String, Int>()
+
     // Keep track of variable names encountered to prevent possible double-binding
     private val seenVarNames = mutableListOf<String>()
+
     // Map of all QuantifiedVariables to be renamed
     private val replacementMap = mutableMapOf<QuantifiedVariable, String>()
 
@@ -114,7 +116,7 @@ class UniqueVariables : DoNothingVisitor() {
  */
 class VariableRenamer(
     private val replacementMap: Map<QuantifiedVariable, String>,
-    val strict: Boolean = true
+    val strict: Boolean = true,
 ) : FirstOrderTermVisitor<Unit>() {
     /**
      * Change the variable name to the new spelling
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt b/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt
index ab6685231..27a9b90af 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt
@@ -41,7 +41,7 @@ class Unification {
         private fun findTermsToUnify(
             terms: MutableList<Pair<FirstOrderTerm, FirstOrderTerm>>,
             r1: Relation,
-            r2: Relation
+            r2: Relation,
         ) {
             val arg1 = r1.arguments
             val arg2 = r2.arguments
@@ -69,7 +69,6 @@ class Unification {
 
             // As long as both relations aren't the same
             while (terms.isNotEmpty()) {
-
                 var (term1, term2) = terms.removeAt(0)
 
                 // Apply gathered substitutions just-in-time
diff --git a/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt b/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt
index a18e5745e..9a69d851d 100644
--- a/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt
+++ b/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt
@@ -62,7 +62,7 @@ class UnifierEquivalence {
          * @return List of pairs of terms with canonical names applied
          */
         private fun canonicalVarNames(
-            list: List<Pair<FirstOrderTerm, FirstOrderTerm>>
+            list: List<Pair<FirstOrderTerm, FirstOrderTerm>>,
         ): List<Pair<FirstOrderTerm, FirstOrderTerm>> {
             val canon1 = VariableCanonicizer()
             val canon2 = VariableCanonicizer()
diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt
index 230874ced..9d10c94b9 100644
--- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt
+++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt
@@ -210,7 +210,7 @@ fun applyClose(
     state: NcTableauxState,
     nodeID: Int,
     closeID: Int,
-    varAssign: Map<String, FirstOrderTerm>?
+    varAssign: Map<String, FirstOrderTerm>?,
 ): NcTableauxState {
     checkCloseIDRestrictions(state, nodeID, closeID)
 
@@ -243,7 +243,7 @@ fun applyClose(
     if (!nodeRelation.synEq(closeRelation)) {
         throw IllegalMove(
             "Relations '$nodeRelation' and '$closeRelation' are" +
-                " not equal after variable instantiation"
+                " not equal after variable instantiation",
         )
     }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt
index e6d37d83e..b11898bd5 100644
--- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt
+++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt
@@ -16,7 +16,7 @@ import kalkulierbar.logic.transform.FreeVariableCollector
  */
 class DeltaSkolemization(
     private val toReplace: List<QuantifiedVariable>,
-    private val term: FirstOrderTerm
+    private val term: FirstOrderTerm,
 ) : DoNothingVisitor() {
 
     companion object Companion {
@@ -29,7 +29,7 @@ class DeltaSkolemization(
         fun transform(
             formula: ExistentialQuantifier,
             blacklist: MutableSet<String>,
-            skolemCounter: Int
+            skolemCounter: Int,
         ): LogicNode {
             // Collect free variables in formula
             val freeVariables = FreeVariableCollector.collect(formula)
@@ -50,7 +50,7 @@ class DeltaSkolemization(
         private fun getSkolemTerm(
             skolemBaseCount: Int,
             nameBlacklist: MutableSet<String>,
-            freeVariables: Set<QuantifiedVariable>
+            freeVariables: Set<QuantifiedVariable>,
         ): FirstOrderTerm {
             var skolemCounter = skolemBaseCount
             var skolemName = "sk$skolemCounter"
@@ -96,7 +96,7 @@ class DeltaSkolemization(
  */
 class DeltaSkolemTermReplacer(
     private val toReplace: List<QuantifiedVariable>,
-    private val term: FirstOrderTerm
+    private val term: FirstOrderTerm,
 ) : FirstOrderTermVisitor<FirstOrderTerm>() {
 
     /**
diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt
index 5a0492b6c..2f26e91fd 100644
--- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt
+++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt
@@ -54,7 +54,7 @@ class DeltaMove(val nodeID: Int) : NcTableauxMove() {
 class CloseMove(
     val nodeID: Int,
     val closeID: Int,
-    val varAssign: Map<String, String>?
+    val varAssign: Map<String, String>?,
 ) : NcTableauxMove() {
     /**
      * Parses map values to first-order terms
diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt
index 39928caa0..0574c95d1 100644
--- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt
+++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt
@@ -10,7 +10,7 @@ import kotlinx.serialization.Serializable
 @Serializable
 class NcTableauxState(
     val formula: LogicNode,
-    val backtracking: Boolean = true
+    val backtracking: Boolean = true,
 ) : ProtectedState(), TreeGardener<NcTableauxNode> {
     override val tree = mutableListOf(NcTableauxNode(null, formula.clone()))
     val moveHistory = mutableListOf<NcTableauxMove>()
@@ -67,7 +67,7 @@ class NcTableauxState(
 @Serializable
 class NcTableauxNode(
     override var parent: Int?,
-    var formula: LogicNode
+    var formula: LogicNode,
 ) : GenericTreeNode {
 
     var isClosed = false
diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt
index e9d56ebd2..11ea04633 100644
--- a/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt
+++ b/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt
@@ -26,9 +26,8 @@ object ClauseSetParser {
         formula: String,
         clauseSeparator: String,
         atomSeparator: String,
-        negSign: Char
+        negSign: Char,
     ): ClauseSet<String> {
-
         val aSep = Regex.escape(atomSeparator)
         val cSep = Regex.escape(clauseSeparator)
         val nSig = Regex.escape(negSign.toString())
@@ -49,7 +48,7 @@ object ClauseSetParser {
         if (!(Regex(formulaFormat) matches pf)) {
             throw InvalidFormulaFormat(
                 "Please use alphanumeric variables only, " +
-                    "separate atoms with '$atomSeparator' and clauses with '$clauseSeparator'."
+                    "separate atoms with '$atomSeparator' and clauses with '$clauseSeparator'.",
             )
         }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt
index a8e201139..d5f8ce612 100644
--- a/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt
+++ b/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt
@@ -133,7 +133,6 @@ class FirstOrderParser : PropositionalParser() {
      * @return LogicNode representing the series of quantifiers
      */
     private fun parseQuantifier(): LogicNode {
-
         if (!nextTokenIs(TokenType.UNIVERSALQUANT) && !nextTokenIs(TokenType.EXISTENTIALQUANT)) {
             return parseParen()
         }
@@ -207,7 +206,7 @@ class FirstOrderParser : PropositionalParser() {
 
         // Relation may have an arbitrary amount of argument terms
         val arguments = mutableListOf<FirstOrderTerm>()
-        if (! nextTokenIs(TokenType.RPAREN)) {
+        if (!nextTokenIs(TokenType.RPAREN)) {
             arguments.add(parseTerm())
         }
         while (nextTokenIs(TokenType.COMMA)) {
diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt
index 36b229f9d..968f57dad 100644
--- a/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt
+++ b/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt
@@ -38,7 +38,6 @@ object FlexibleClauseSetParser {
         try {
             return convertToCNF(PropositionalParser().parse(formula), strategy)
         } catch (e: InvalidFormulaFormat) {
-
             // If the input formula is likely intended to be certain input type, only report that error
             if (likelyFormula && !likelyClauseSet) {
                 errorMsg = ""
diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt b/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt
index 761cf9257..32f1800c5 100644
--- a/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt
+++ b/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt
@@ -52,7 +52,7 @@ class Tokenizer {
             formula: String,
             index: Int,
             tokens: MutableList<Token>,
-            positionInBaseString: Int
+            positionInBaseString: Int,
         ): Int {
             var i = index
             val len = formula.length
diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt
index 2fd5e2ac6..fc8404efd 100644
--- a/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt
+++ b/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt
@@ -11,7 +11,6 @@ import kalkulierbar.logic.transform.VariableInstantiator
 import kalkulierbar.logic.util.Unification
 import kalkulierbar.logic.util.UnifierEquivalence
 
-@Suppress("ThrowsCount", "LongParameterList")
 /**
  * Resolve two clauses by unifying two literals by a given variable assignment or automatically
  * @param state Current proof state
@@ -21,13 +20,14 @@ import kalkulierbar.logic.util.UnifierEquivalence
  * @param c2lit The literal to unify of the second clause
  * @param varAssign Variable assignment to be used
  */
+@Suppress("ThrowsCount", "LongParameterList")
 fun resolveMove(
     state: FoResolutionState,
     c1: Int,
     c2: Int,
     c1lit: Int,
     c2lit: Int,
-    varAssign: Map<String, FirstOrderTerm>?
+    varAssign: Map<String, FirstOrderTerm>?,
 ) {
     resolveCheckID(state, c1, c2, c1lit, c2lit)
 
@@ -80,7 +80,7 @@ fun resolveMove(
 private fun instantiate(
     state: FoResolutionState,
     clauseID: Int,
-    varAssign: Map<String, FirstOrderTerm>
+    varAssign: Map<String, FirstOrderTerm>,
 ) {
     if (clauseID < 0 || clauseID >= state.clauseSet.clauses.size) {
         throw IllegalMove("There is no clause with id $clauseID")
@@ -101,7 +101,7 @@ private fun instantiate(
  */
 private fun instantiateReturn(
     baseClause: Clause<Relation>,
-    varAssign: Map<String, FirstOrderTerm>
+    varAssign: Map<String, FirstOrderTerm>,
 ): Clause<Relation> {
     val newClause = Clause<Relation>()
 
@@ -120,7 +120,7 @@ private fun instantiateReturn(
  */
 private fun instantiateReturn(
     baseAtom: Atom<Relation>,
-    varAssign: Map<String, FirstOrderTerm>
+    varAssign: Map<String, FirstOrderTerm>,
 ): Atom<Relation> {
     val instantiator = VariableInstantiator(varAssign)
     val relationArgs = baseAtom.lit.arguments.map { it.clone().accept(instantiator) }
@@ -162,7 +162,7 @@ fun factorize(state: FoResolutionState, clauseID: Int, atomIDs: List<Int>) {
             if (newClause.atoms[firstID] != newClause.atoms[secondID]) {
                 throw IllegalMove(
                     "Atoms '${newClause.atoms[firstID]}' and '${newClause.atoms[secondID]}'" +
-                        " are not equal after instantiation"
+                        " are not equal after instantiation",
                 )
             }
 
@@ -192,7 +192,7 @@ fun factorize(state: FoResolutionState, clauseID: Int, atomIDs: List<Int>) {
 fun hyper(
     state: FoResolutionState,
     mainID: Int,
-    atomMap: Map<Int, Pair<Int, Int>>
+    atomMap: Map<Int, Pair<Int, Int>>,
 ) {
     // Checks for correct clauseID and IDs in Map
     checkHyperID(state, mainID, atomMap)
@@ -226,7 +226,7 @@ fun hyper(
     } catch (e: UnificationImpossible) {
         throw IllegalMove(
             "Could not unify main premiss with " +
-                "the side premises: ${e.message}"
+                "the side premises: ${e.message}",
         )
     }
 
@@ -241,7 +241,7 @@ fun hyper(
             newMainPremiss,
             instantiateReturn(mainPremiss.atoms[mAtomID], mgu),
             newSidePremis,
-            newSidePremis.atoms[sAtomID]
+            newSidePremis.atoms[sAtomID],
         )
     }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderResolution.kt b/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderResolution.kt
index a3a0e7769..3131f16c3 100644
--- a/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderResolution.kt
+++ b/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderResolution.kt
@@ -21,7 +21,10 @@ class FirstOrderResolution :
     JSONCalculus<FoResolutionState, ResolutionMove, FoResolutionParam>() {
     override val identifier = "fo-resolution"
 
-    override val serializer = Json { serializersModule = resolutionMoveModule + FoTermModule; encodeDefaults = true }
+    override val serializer = Json {
+        serializersModule = resolutionMoveModule + FoTermModule
+        encodeDefaults = true
+    }
     override val stateSerializer = FoResolutionState.serializer()
     override val moveSerializer = ResolutionMove.serializer()
 
@@ -77,7 +80,7 @@ class FirstOrderResolution :
 @Serializable
 class FoResolutionState(
     override val clauseSet: ClauseSet<Relation>,
-    override val visualHelp: VisualHelp
+    override val visualHelp: VisualHelp,
 ) : GenericResolutionState<Relation>, ProtectedState() {
     override var newestNode = -1
     override val hiddenClauses = ClauseSet<Relation>()
diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt b/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt
index 0860091c1..35e268807 100644
--- a/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt
+++ b/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt
@@ -34,7 +34,7 @@ interface GenericResolutionState<AtomType> {
         clause1: Int,
         clause2: Int,
         literal: AtomType?,
-        insertAtEnd: Boolean = false
+        insertAtEnd: Boolean = false,
     ) {
         val clauses = clauseSet.clauses
 
diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt b/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt
index b6cfd7ec3..9490cb311 100644
--- a/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt
+++ b/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt
@@ -16,7 +16,7 @@ import kalkulierbar.logic.SyntacticEquality
 fun <AtomType> filterClause(
     c1: Clause<AtomType>,
     c2: Clause<AtomType>,
-    literal: AtomType
+    literal: AtomType,
 ): Pair<Atom<AtomType>, Atom<AtomType>> {
     // Filter clauses for atoms with correct literal
     val atomsInC1 = c1.atoms.filter { literalsAreEqual(it.lit, literal) }
@@ -40,9 +40,8 @@ fun <AtomType> filterClause(
  */
 fun <AtomType> getAutoResolutionCandidates(
     c1: Clause<AtomType>,
-    c2: Clause<AtomType>
+    c2: Clause<AtomType>,
 ): Pair<Atom<AtomType>, Atom<AtomType>> {
-
     // Find literals present in both clauses
     var sharedAtoms = c1.atoms.filter { c1atom ->
         c2.atoms.any { literalsAreEqual(c1atom.lit, it.lit) }
@@ -60,7 +59,7 @@ fun <AtomType> getAutoResolutionCandidates(
     if (sharedAtoms.isEmpty()) {
         throw IllegalMove(
             "Clauses '$c1' and '$c2' contain no common literals that appear" +
-                "in positive and negated form"
+                "in positive and negated form",
         )
     }
 
@@ -83,7 +82,7 @@ fun <AtomType> buildClause(
     c1: Clause<AtomType>,
     a1: Atom<AtomType>,
     c2: Clause<AtomType>,
-    a2: Atom<AtomType>
+    a2: Atom<AtomType>,
 ): Clause<AtomType> {
     val atoms = c1.atoms.filter { it != a1 }.toMutableList() +
         c2.atoms.filter { it != a2 }.toMutableList()
@@ -99,7 +98,7 @@ fun <AtomType> buildClause(
  */
 fun <AtomType> findResCandidates(
     atoms1: List<Atom<AtomType>>,
-    atoms2: List<Atom<AtomType>>
+    atoms2: List<Atom<AtomType>>,
 ): Pair<Atom<AtomType>, Atom<AtomType>>? {
     val (pos, neg) = atoms2.partition { !it.negated }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt b/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt
index 2c59bedeb..946aff1bd 100644
--- a/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt
+++ b/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt
@@ -15,7 +15,10 @@ class PropositionalResolution : GenericResolution<String>,
     JSONCalculus<ResolutionState, ResolutionMove, ResolutionParam>() {
     override val identifier = "prop-resolution"
 
-    override val serializer = Json { serializersModule = resolutionMoveModule; encodeDefaults = true }
+    override val serializer = Json {
+        serializersModule = resolutionMoveModule
+        encodeDefaults = true
+    }
     override val stateSerializer = ResolutionState.serializer()
     override val moveSerializer = ResolutionMove.serializer()
 
@@ -80,7 +83,7 @@ class PropositionalResolution : GenericResolution<String>,
     fun hyper(
         state: ResolutionState,
         mainID: Int,
-        atomMap: Map<Int, Pair<Int, Int>>
+        atomMap: Map<Int, Pair<Int, Int>>,
     ) {
         // Checks for correct clauseID and IDs in Map
         checkHyperID(state, mainID, atomMap)
@@ -140,7 +143,7 @@ class PropositionalResolution : GenericResolution<String>,
 @Serializable
 class ResolutionState(
     override val clauseSet: ClauseSet<String>,
-    override val visualHelp: VisualHelp
+    override val visualHelp: VisualHelp,
 ) : GenericResolutionState<String>, ProtectedState() {
     override var newestNode = -1
     override val hiddenClauses = ClauseSet<String>()
diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/ResolutionMove.kt b/backend/src/main/kotlin/kalkulierbar/resolution/ResolutionMove.kt
index 3bf2cc90e..91a96f8ca 100644
--- a/backend/src/main/kotlin/kalkulierbar/resolution/ResolutionMove.kt
+++ b/backend/src/main/kotlin/kalkulierbar/resolution/ResolutionMove.kt
@@ -40,7 +40,7 @@ data class MoveResolveCustom(
     val c2: Int,
     val l1: Int,
     val l2: Int,
-    val varAssign: Map<String, String>
+    val varAssign: Map<String, String>,
 ) : ResolutionMove() {
     fun getVarAssignTerms() = varAssign.mapValues {
         try {
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculus.kt b/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculus.kt
index 7f66a2a87..3ace85a1d 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculus.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculus.kt
@@ -52,19 +52,19 @@ class TreeNode(
     val leftFormulas: MutableList<LogicNode>,
     val rightFormulas: MutableList<LogicNode>,
     var isClosed: Boolean,
-    val lastMove: SequentCalculusMove?
+    val lastMove: SequentCalculusMove?,
 
 ) : GenericTreeNode {
     constructor(
         parent: Int,
         leftFormulas: MutableList<LogicNode>,
         rightFormulas: MutableList<LogicNode>,
-        lastMove: SequentCalculusMove
+        lastMove: SequentCalculusMove,
     ) : this (parent, mutableListOf(), leftFormulas, rightFormulas, false, lastMove)
 
     constructor(
         leftFormulas: MutableList<LogicNode>,
-        rightFormulas: MutableList<LogicNode>
+        rightFormulas: MutableList<LogicNode>,
     ) : this(null, mutableListOf(), leftFormulas, rightFormulas, false, null)
 
     override fun toString(): String {
@@ -74,5 +74,5 @@ class TreeNode(
 
 @Serializable
 data class SequentCalculusParam(
-    val showOnlyApplicableRules: Boolean
+    val showOnlyApplicableRules: Boolean,
 )
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt
index 7165ff96d..5ad8b3f4d 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt
@@ -14,7 +14,6 @@ import kalkulierbar.logic.Or
  */
 @Suppress("ThrowsCount")
 fun applyAx(state: GenericSequentCalculusState, nodeID: Int): GenericSequentCalculusState {
-
     state.checkNodeID(nodeID)
     val leaf = state.tree[nodeID]
 
@@ -29,7 +28,7 @@ fun applyAx(state: GenericSequentCalculusState, nodeID: Int): GenericSequentCalc
                 mutableListOf(),
                 mutableListOf(),
                 true,
-                Ax(nodeID)
+                Ax(nodeID),
             )
             state.addChildren(nodeID, newLeaf)
             state.setNodeClosed(newLeaf)
@@ -65,7 +64,7 @@ fun applyNotRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: In
         nodeID,
         newLeftFormula.distinct().toMutableList(),
         newRightFormula.distinct().toMutableList(),
-        NotRight(nodeID, listIndex)
+        NotRight(nodeID, listIndex),
     )
     state.addChildren(nodeID, newLeaf)
     return state
@@ -80,7 +79,6 @@ fun applyNotRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: In
  * @return new state after applying move
  */
 fun applyNotLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState {
-
     checkLeft(state, nodeID, listIndex)
 
     val leaf = state.tree[nodeID]
@@ -98,7 +96,7 @@ fun applyNotLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
         nodeID,
         newLeftFormula.distinct().toMutableList(),
         newRightFormula.distinct().toMutableList(),
-        NotLeft(nodeID, listIndex)
+        NotLeft(nodeID, listIndex),
     )
     state.addChildren(nodeID, newLeaf)
     return state
@@ -113,7 +111,6 @@ fun applyNotLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
  * @return new state after applying move
  */
 fun applyOrRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState {
-
     checkRight(state, nodeID, listIndex)
 
     val leaf = state.tree[nodeID]
@@ -131,7 +128,7 @@ fun applyOrRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
         nodeID,
         newLeftFormula.distinct().toMutableList(),
         newRightFormula.distinct().toMutableList(),
-        OrRight(nodeID, listIndex)
+        OrRight(nodeID, listIndex),
     )
     state.addChildren(nodeID, newLeaf)
     return state
@@ -150,7 +147,6 @@ fun applyOrRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
  * @return new state after applying move
  */
 fun applyOrLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState {
-
     checkLeft(state, nodeID, listIndex)
 
     val leaf = state.tree[nodeID]
@@ -173,13 +169,13 @@ fun applyOrLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int)
         nodeID,
         newLeftFormulaOnLeftChild.distinct().toMutableList(),
         newRightFormulaOnLeftChild.distinct().toMutableList(),
-        OrLeft(nodeID, listIndex)
+        OrLeft(nodeID, listIndex),
     )
     val newRightLeaf = TreeNode(
         nodeID,
         newLeftFormulaOnRightChild.distinct().toMutableList(),
         newRightFormulaOnRightChild.distinct().toMutableList(),
-        OrLeft(nodeID, listIndex)
+        OrLeft(nodeID, listIndex),
     )
 
     state.addChildren(nodeID, newLeftLeaf, newRightLeaf)
@@ -199,7 +195,6 @@ fun applyOrLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int)
  * @return new state after applying move
  */
 fun applyAndRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState {
-
     checkRight(state, nodeID, listIndex)
 
     val leaf = state.tree[nodeID]
@@ -222,13 +217,13 @@ fun applyAndRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: In
         nodeID,
         newLeftFormulaOnLeftChild.distinct().toMutableList(),
         newRightFormulaOnLeftChild.distinct().toMutableList(),
-        AndRight(nodeID, listIndex)
+        AndRight(nodeID, listIndex),
     )
     val newRightLeaf = TreeNode(
         nodeID,
         newLeftFormulaOnRightChild.distinct().toMutableList(),
         newRightFormulaOnRightChild.distinct().toMutableList(),
-        AndRight(nodeID, listIndex)
+        AndRight(nodeID, listIndex),
     )
     state.addChildren(nodeID, newLeftLeaf, newRightLeaf)
 
@@ -244,7 +239,6 @@ fun applyAndRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: In
  * @return new state after applying move
  */
 fun applyAndLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState {
-
     checkLeft(state, nodeID, listIndex)
 
     val leaf = state.tree[nodeID]
@@ -262,7 +256,7 @@ fun applyAndLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
         nodeID,
         newLeftFormula.distinct().toMutableList(),
         newRightFormula.distinct().toMutableList(),
-        AndLeft(nodeID, listIndex)
+        AndLeft(nodeID, listIndex),
     )
     state.addChildren(nodeID, newLeaf)
     return state
@@ -281,7 +275,6 @@ fun applyAndLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
  * @return new state after applying move
  */
 fun applyImpLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState {
-
     checkLeft(state, nodeID, listIndex)
 
     val leaf = state.tree[nodeID]
@@ -303,13 +296,13 @@ fun applyImpLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int
         nodeID,
         newLeftFormulaOnLeftChild.distinct().toMutableList(),
         newRightFormulaOnLeftChild.distinct().toMutableList(),
-        ImpLeft(nodeID, listIndex)
+        ImpLeft(nodeID, listIndex),
     )
     val newRightLeaf = TreeNode(
         nodeID,
         newLeftFormulaOnRightChild.distinct().toMutableList(),
         newRightFormulaOnRightChild.distinct().toMutableList(),
-        ImpLeft(nodeID, listIndex)
+        ImpLeft(nodeID, listIndex),
     )
 
     state.addChildren(nodeID, newLeftLeaf, newRightLeaf)
@@ -343,7 +336,7 @@ fun applyImpRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: In
         nodeID,
         newLeftFormula.distinct().toMutableList(),
         newRightFormula.distinct().toMutableList(),
-        ImpRight(nodeID, listIndex)
+        ImpRight(nodeID, listIndex),
     )
     state.addChildren(nodeID, newLeaf)
     return state
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/SequentCalculusMove.kt b/backend/src/main/kotlin/kalkulierbar/sequent/SequentCalculusMove.kt
index 1b5d1344a..ca5f7042f 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/SequentCalculusMove.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/SequentCalculusMove.kt
@@ -34,63 +34,63 @@ abstract class SequentCalculusMove
 @Serializable
 @SerialName("Ax")
 class Ax(
-    val nodeID: Int
+    val nodeID: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("notRight")
 class NotRight(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("notLeft")
 class NotLeft(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("orRight")
 class OrRight(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("andRight")
 class AndRight(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("orLeft")
 class OrLeft(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("andLeft")
 class AndLeft(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("impLeft")
 class ImpLeft(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
 @SerialName("impRight")
 class ImpRight(
     val nodeID: Int,
-    val listIndex: Int
+    val listIndex: Int,
 ) : SequentCalculusMove()
 
 @Serializable
@@ -100,7 +100,7 @@ class UndoMove : SequentCalculusMove()
 @Serializable
 @SerialName("prune")
 class PruneMove(
-    val nodeID: Int
+    val nodeID: Int,
 ) : SequentCalculusMove()
 
 // FOSC MOVES
@@ -109,7 +109,7 @@ class PruneMove(
 class AllLeft(
     val nodeID: Int,
     val listIndex: Int,
-    val instTerm: String
+    val instTerm: String,
 ) : SequentCalculusMove()
 
 @Serializable
@@ -117,7 +117,7 @@ class AllLeft(
 class AllRight(
     val nodeID: Int,
     val listIndex: Int,
-    val instTerm: String? = null
+    val instTerm: String? = null,
 ) : SequentCalculusMove()
 
 @Serializable
@@ -125,7 +125,7 @@ class AllRight(
 class ExLeft(
     val nodeID: Int,
     val listIndex: Int,
-    val instTerm: String? = null
+    val instTerm: String? = null,
 ) : SequentCalculusMove()
 
 @Serializable
@@ -133,5 +133,5 @@ class ExLeft(
 class ExRight(
     val nodeID: Int,
     val listIndex: Int,
-    val instTerm: String
+    val instTerm: String,
 ) : SequentCalculusMove()
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt
index 7b9393a98..007ac43c4 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt
@@ -54,7 +54,7 @@ fun applyAllLeft(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, ins
         nodeID,
         newLeftFormulas,
         node.rightFormulas.distinct().toMutableList(),
-        AllLeft(nodeID, listIndex, instTerm)
+        AllLeft(nodeID, listIndex, instTerm),
     )
 
     state.addChildren(nodeID, newLeaf)
@@ -75,7 +75,7 @@ fun applyAllRight(
     state: FirstOrderSequentState,
     nodeID: Int,
     listIndex: Int,
-    instTerm: String?
+    instTerm: String?,
 ): FirstOrderSequentState {
     checkRight(state, nodeID, listIndex)
 
@@ -112,7 +112,7 @@ fun applyAllRight(
         nodeID,
         node.leftFormulas.distinct().toMutableList(),
         newRightFormulas,
-        AllRight(nodeID, listIndex, instTerm)
+        AllRight(nodeID, listIndex, instTerm),
     )
 
     state.addChildren(nodeID, newLeaf)
@@ -165,7 +165,7 @@ fun applyExLeft(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, inst
         nodeID,
         newLeftFormulas,
         node.rightFormulas.distinct().toMutableList(),
-        ExLeft(nodeID, listIndex, instTerm)
+        ExLeft(nodeID, listIndex, instTerm),
     )
     state.addChildren(nodeID, newLeaf)
 
@@ -208,7 +208,7 @@ fun applyExRight(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, ins
         nodeID,
         node.leftFormulas.distinct().toMutableList(),
         newRightFormulas,
-        ExRight(nodeID, listIndex, instTerm)
+        ExRight(nodeID, listIndex, instTerm),
     )
     state.addChildren(nodeID, newLeaf)
 
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt b/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt
index 9c7c65c38..f02eb249c 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt
@@ -57,7 +57,7 @@ class FirstOrderSequent :
         val sequents = FirstOrderSequentParser.parse(formula)
         return FirstOrderSequentState(
             mutableListOf(TreeNode(sequents.first.toMutableList(), sequents.second.toMutableList())),
-            params?.showOnlyApplicableRules ?: false
+            params?.showOnlyApplicableRules ?: false,
         )
     }
 
@@ -109,7 +109,7 @@ class FirstOrderSequent :
 
     override fun scoreFromState(
         state: FirstOrderSequentState,
-        name: String?
+        name: String?,
     ): Map<String, String> = stateToStat(state, name)
     override fun formulaFromState(state: FirstOrderSequentState) = state.tree[0].toString()
 }
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequentState.kt b/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequentState.kt
index 62254b59f..ae036d089 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequentState.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequentState.kt
@@ -8,7 +8,7 @@ import kotlinx.serialization.Serializable
 @Serializable
 class FirstOrderSequentState(
     override val tree: MutableList<TreeNode> = mutableListOf(),
-    override var showOnlyApplicableRules: Boolean = false
+    override var showOnlyApplicableRules: Boolean = false,
 ) : GenericSequentCalculusState, ProtectedState() {
     override var seal = ""
 
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt b/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt
index 61a360ce7..6d4e622bb 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt
@@ -51,14 +51,14 @@ class PropositionalSequent : GenericSequentCalculus,
         val sequents = PropositionalSequentParser.parse(formula)
         return PropositionalSequentState(
             mutableListOf(TreeNode(sequents.first.toMutableList(), sequents.second.toMutableList())),
-            params?.showOnlyApplicableRules ?: false
+            params?.showOnlyApplicableRules ?: false,
         )
     }
 
     @Suppress("ComplexMethod")
     override fun applyMoveOnState(
         state: PropositionalSequentState,
-        move: SequentCalculusMove
+        move: SequentCalculusMove,
     ): PropositionalSequentState {
         // Pass moves to relevant subfunction
         return when (move) {
@@ -102,7 +102,7 @@ class PropositionalSequent : GenericSequentCalculus,
 
     override fun scoreFromState(
         state: PropositionalSequentState,
-        name: String?
+        name: String?,
     ): Map<String, String> = stateToStat(state, name)
     override fun formulaFromState(state: PropositionalSequentState) = state.tree[0].toString()
 }
diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequentState.kt b/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequentState.kt
index 192deaba2..a57677df0 100644
--- a/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequentState.kt
+++ b/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequentState.kt
@@ -8,7 +8,7 @@ import kotlinx.serialization.Serializable
 @Serializable
 class PropositionalSequentState(
     override val tree: MutableList<TreeNode> = mutableListOf(),
-    override var showOnlyApplicableRules: Boolean = false
+    override var showOnlyApplicableRules: Boolean = false,
 ) : GenericSequentCalculusState, ProtectedState() {
     override var seal = ""
 
diff --git a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt
index c287e25b9..e3788a2c0 100644
--- a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt
+++ b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt
@@ -39,7 +39,7 @@ class SignedModalTableaux :
     @Suppress("ComplexMethod")
     override fun applyMoveOnState(
         state: SignedModalTableauxState,
-        move: SignedModalTableauxMove
+        move: SignedModalTableauxMove,
     ): SignedModalTableauxState {
         // Clear status message
         state.statusMessage = null
diff --git a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt
index 552b9e93e..283c3b2d9 100644
--- a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt
+++ b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt
@@ -10,7 +10,7 @@ import kotlinx.serialization.Serializable
 class SignedModalTableauxState(
     val formula: LogicNode,
     val assumption: Boolean,
-    val backtracking: Boolean
+    val backtracking: Boolean,
 ) : ProtectedState(), TreeGardener<SignedModalTableauxNode> {
     override val tree = mutableListOf(SignedModalTableauxNode(null, listOf(1), assumption, formula.clone()))
     val moveHistory = mutableListOf<SignedModalTableauxMove>()
@@ -84,7 +84,7 @@ class SignedModalTableauxNode(
     override var parent: Int?,
     var prefix: List<Int>,
     var sign: Boolean,
-    var formula: LogicNode
+    var formula: LogicNode,
 ) : GenericTreeNode {
     var isClosed = false
     var closeRef: Int? = null
@@ -102,5 +102,5 @@ class SignedModalTableauxNode(
 
 @Serializable
 data class SignedModalTableauxParam(
-    val backtracking: Boolean
+    val backtracking: Boolean,
 )
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt
index bc3f7bfd8..9e7e33e38 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt
@@ -45,7 +45,7 @@ fun applyMoveCloseBranch(
     state: FoTableauxState,
     leafID: Int,
     closeNodeID: Int,
-    varAssign: Map<String, FirstOrderTerm>
+    varAssign: Map<String, FirstOrderTerm>,
 ): FoTableauxState {
     ensureBasicCloseability(state, leafID, closeNodeID)
 
@@ -76,9 +76,8 @@ private fun closeBranchCommon(
     state: FoTableauxState,
     leafID: Int,
     closeNodeID: Int,
-    varAssign: Map<String, FirstOrderTerm>
+    varAssign: Map<String, FirstOrderTerm>,
 ): FoTableauxState {
-
     val leaf = state.tree[leafID]
     val closeNode = state.tree[closeNodeID]
 
@@ -115,7 +114,6 @@ private fun closeBranchCommon(
  * @return State with the expansion applied
  */
 fun applyMoveExpandLeaf(state: FoTableauxState, leafID: Int, clauseID: Int): FoTableauxState {
-
     // Ensure that preconditions (correct indices, regularity) are met
     ensureExpandability(state, leafID, clauseID)
     val clause = state.clauseSet.clauses[clauseID]
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt
index a890e5f84..5386761ed 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt
@@ -35,7 +35,7 @@ class FirstOrderTableaux : GenericTableaux<Relation>, JSONCalculus<FoTableauxSta
             params.type,
             params.regular,
             params.backtracking,
-            params.manualVarAssign
+            params.manualVarAssign,
         )
     }
 
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableauxMisc.kt
index bc2c0f086..a97a0c66b 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableauxMisc.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableauxMisc.kt
@@ -20,7 +20,7 @@ class FoTableauxState(
     override val type: TableauxType = TableauxType.UNCONNECTED,
     override val regular: Boolean = false,
     override val backtracking: Boolean = false,
-    val manualVarAssign: Boolean = false
+    val manualVarAssign: Boolean = false,
 ) : GenericTableauxState<Relation>, ProtectedState() {
     override val tree = mutableListOf(FoTableauxNode(null, Relation("true", listOf()), false))
     val moveHistory = mutableListOf<TableauxMove>()
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt
index 6deb1b70e..8a7a6f113 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt
@@ -11,7 +11,6 @@ import kalkulierbar.IllegalMove
  * @return New state after rule was applied
  */
 fun applyMoveCloseBranch(state: TableauxState, leafID: Int, closeNodeID: Int): TableauxState {
-
     ensureBasicCloseability(state, leafID, closeNodeID)
 
     val leaf = state.tree[leafID]
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableaux.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableaux.kt
index 2ca3ac4e8..38a2bb15a 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableaux.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableaux.kt
@@ -16,7 +16,10 @@ class PropositionalTableaux : GenericTableaux<String>, JSONCalculus<TableauxStat
 
     override val identifier = "prop-tableaux"
 
-    override val serializer = Json { serializersModule = tableauxMoveModule; encodeDefaults = true }
+    override val serializer = Json {
+        serializersModule = tableauxMoveModule
+        encodeDefaults = true
+    }
     override val stateSerializer = TableauxState.serializer()
     override val moveSerializer = TableauxMove.serializer()
 
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt
index 3f2718d9b..636f2dd84 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt
@@ -16,7 +16,7 @@ class TableauxState(
     override val clauseSet: ClauseSet<String>,
     override val type: TableauxType = TableauxType.UNCONNECTED,
     override val regular: Boolean = false,
-    override val backtracking: Boolean = false
+    override val backtracking: Boolean = false,
 ) : GenericTableauxState<String>, ProtectedState() {
     override val tree = mutableListOf(TableauxNode(null, "true", false))
     val moveHistory = mutableListOf<TableauxMove>()
@@ -96,7 +96,7 @@ class TableauxNode(
     override val parent: Int?,
     override val spelling: String,
     override val negated: Boolean,
-    override val lemmaSource: Int? = null
+    override val lemmaSource: Int? = null,
 ) : GenericTableauxNode<String> {
 
     override var isClosed = false
@@ -139,7 +139,7 @@ data class TableauxParam(
     val type: TableauxType,
     val regular: Boolean,
     val backtracking: Boolean,
-    val cnfStrategy: CnfStrategy = CnfStrategy.OPTIMAL
+    val cnfStrategy: CnfStrategy = CnfStrategy.OPTIMAL,
 )
 
 enum class TableauxType {
diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt
index 293fcd780..31c40e0d8 100644
--- a/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt
+++ b/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt
@@ -16,7 +16,7 @@ fun <AtomType> verifyExpandRegularity(
     state: GenericTableauxState<AtomType>,
     leafID: Int,
     clause: Clause<AtomType>,
-    applyPreprocessing: Boolean = true
+    applyPreprocessing: Boolean = true,
 ) {
     // Create list of predecessor
     val leaf = state.tree[leafID]
@@ -41,7 +41,7 @@ fun <AtomType> verifyExpandRegularity(
         if (lst.contains(atom)) {
             throw IllegalMove(
                 "Expanding this clause would introduce a duplicate " +
-                    "node '$atom' on the branch, making the tree irregular"
+                    "node '$atom' on the branch, making the tree irregular",
             )
         }
     }
@@ -72,7 +72,7 @@ fun <AtomType> verifyExpandConnectedness(state: GenericTableauxState<AtomType>,
                 """
                     No literal in this clause would be closeable with '$leaf',
                     making the tree not strongly connected
-                """
+                """,
             )
         }
     }
@@ -113,7 +113,7 @@ fun <AtomType> checkConnectedness(state: GenericTableauxState<AtomType>, ctype:
 private fun <AtomType> checkConnectedSubtree(
     state: GenericTableauxState<AtomType>,
     root: Int,
-    strong: Boolean
+    strong: Boolean,
 ): Boolean {
     val node = state.tree[root]
 
@@ -171,7 +171,7 @@ fun <AtomType> checkRegularity(state: GenericTableauxState<AtomType>): Boolean {
 private fun <AtomType> checkRegularitySubtree(
     state: GenericTableauxState<AtomType>,
     root: Int,
-    lst: List<Atom<AtomType>>
+    lst: List<Atom<AtomType>>,
 ): Boolean {
     val node = state.tree[root]
 
@@ -205,7 +205,7 @@ fun <AtomType> ensureExpandability(state: GenericTableauxState<AtomType>, leafID
     if (!checkConnectedness(state, state.type)) {
         throw IllegalMove(
             "The proof tree is currently not sufficiently connected, " +
-                "please close branches first to restore connectedness before expanding more leaves"
+                "please close branches first to restore connectedness before expanding more leaves",
         )
     }
     // Verify that both leaf and clause are valid
diff --git a/backend/src/main/kotlin/statekeeper/Scoreboard.kt b/backend/src/main/kotlin/statekeeper/Scoreboard.kt
index 00d4475ba..6ca6c2121 100644
--- a/backend/src/main/kotlin/statekeeper/Scoreboard.kt
+++ b/backend/src/main/kotlin/statekeeper/Scoreboard.kt
@@ -54,7 +54,10 @@ object Scoreboard {
             cleanScoreboards()
         }
         val calculusScores = data.getOrPut(calculus) { mutableMapOf() }
-        val formulaScores = calculusScores.getOrPut(formula) { scoreboardCounter += 1; mutableListOf() }
+        val formulaScores = calculusScores.getOrPut(formula) {
+            scoreboardCounter += 1
+            mutableListOf()
+        }
 
         insertScore(formulaScores, score)
 
diff --git a/backend/src/main/kotlin/statekeeper/Statekeeper.kt b/backend/src/main/kotlin/statekeeper/Statekeeper.kt
index 5ef1cae2c..4f6546a36 100644
--- a/backend/src/main/kotlin/statekeeper/Statekeeper.kt
+++ b/backend/src/main/kotlin/statekeeper/Statekeeper.kt
@@ -231,7 +231,7 @@ object StateKeeper {
 data class AppState(
     val key: String = "WildFlowers/UncomfortableMoons",
     val disabledCalculi: MutableList<String> = mutableListOf(),
-    val examples: MutableList<Example> = mutableListOf()
+    val examples: MutableList<Example> = mutableListOf(),
 )
 
 @Serializable
@@ -240,7 +240,7 @@ data class Example(
     val description: String,
     val calculus: String,
     val formula: String,
-    val params: String
+    val params: String,
 )
 
 class AuthenticationException(msg: String) : KalkulierbarException(msg)
diff --git a/backend/src/main/kotlin/statekeeper/Stats.kt b/backend/src/main/kotlin/statekeeper/Stats.kt
index 69002d066..c872cd4ff 100644
--- a/backend/src/main/kotlin/statekeeper/Stats.kt
+++ b/backend/src/main/kotlin/statekeeper/Stats.kt
@@ -66,7 +66,7 @@ data class StatContainer(
     var currentMonth: MutableMap<String, Int> = mutableMapOf(),
     var lastMonth: Map<String, Int> = mapOf(),
     val alltime: MutableMap<String, Int> = mutableMapOf(),
-    var monthIndex: Int = LocalDateTime.now().monthValue
+    var monthIndex: Int = LocalDateTime.now().monthValue,
 ) {
     fun logHit(key: String) {
         val month = LocalDateTime.now().monthValue
diff --git a/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt b/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt
index 018acff4b..4dbd42a48 100644
--- a/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt
+++ b/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt
@@ -23,7 +23,7 @@ class TestTamperProtect {
         "lightbulb",
         "shine",
         "dim",
-        "utopia"
+        "utopia",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/dpll/TestSplit.kt b/backend/src/test/kotlin/kalkulierbar/dpll/TestSplit.kt
index 82a770962..c09c5dcc7 100644
--- a/backend/src/test/kotlin/kalkulierbar/dpll/TestSplit.kt
+++ b/backend/src/test/kotlin/kalkulierbar/dpll/TestSplit.kt
@@ -66,15 +66,15 @@ class TestSplit {
         assertEquals("[{!a}, {b, c}, {b}, {a}]", state.tree[1].diff.apply(state.clauseSet).clauses.toString())
         assertEquals(
             "[{!a}, {b, c}, {b}, {!a}]",
-            state.tree[2].diff.apply(state.clauseSet).clauses.toString()
+            state.tree[2].diff.apply(state.clauseSet).clauses.toString(),
         )
         assertEquals(
             "[{!a}, {b, c}, {b}, {b}]",
-            state.tree[3].diff.apply(state.clauseSet).clauses.toString()
+            state.tree[3].diff.apply(state.clauseSet).clauses.toString(),
         )
         assertEquals(
             "[{!a}, {b, c}, {b}, {!b}]",
-            state.tree[4].diff.apply(state.clauseSet).clauses.toString()
+            state.tree[4].diff.apply(state.clauseSet).clauses.toString(),
         )
     }
 
diff --git a/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestOrRight.kt b/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestOrRight.kt
index 2aa6bf692..a51b39230 100644
--- a/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestOrRight.kt
+++ b/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestOrRight.kt
@@ -30,6 +30,7 @@ class TestOrRight {
         assertTrue(node1.rightFormulas[0] is Relation)
         assertTrue(node1.rightFormulas[1] is Relation)
     }
+
     @Test
     fun testParent() {
         var state = instance.parseFormulaToState("P(a) | P(b)", null)
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/TestFOLogic.kt b/backend/src/test/kotlin/kalkulierbar/logic/TestFOLogic.kt
index da217728a..f5b70de81 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/TestFOLogic.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/TestFOLogic.kt
@@ -34,10 +34,10 @@ class TestFOLogic {
                     "f",
                     listOf(
                         Constant("d"),
-                        QuantifiedVariable("X")
-                    )
-                )
-            )
+                        QuantifiedVariable("X"),
+                    ),
+                ),
+            ),
         )
         r3 = Relation(
             "Aefjwadg",
@@ -47,11 +47,11 @@ class TestFOLogic {
                     listOf(
                         Function(
                             "f",
-                            listOf(Constant("c"), Constant("k"))
-                        )
-                    )
-                )
-            )
+                            listOf(Constant("c"), Constant("k")),
+                        ),
+                    ),
+                ),
+            ),
         )
 
         u1 = UniversalQuantifier("X", Or(Var("X"), Not(Var("X"))), mutableListOf())
@@ -66,22 +66,22 @@ class TestFOLogic {
                             "R",
                             listOf(
                                 QuantifiedVariable("X"),
-                                QuantifiedVariable("Y")
-                            )
+                                QuantifiedVariable("Y"),
+                            ),
                         ),
                         Relation(
                             "R",
                             listOf(
                                 QuantifiedVariable("Y"),
-                                QuantifiedVariable("Z")
-                            )
-                        )
+                                QuantifiedVariable("Z"),
+                            ),
+                        ),
                     ),
-                    mutableListOf()
+                    mutableListOf(),
                 ),
-                mutableListOf()
+                mutableListOf(),
             ),
-            mutableListOf()
+            mutableListOf(),
         )
         u3 = UniversalQuantifier(
             "Number1",
@@ -91,12 +91,12 @@ class TestFOLogic {
                     "Greater",
                     listOf(
                         QuantifiedVariable("Number1"),
-                        QuantifiedVariable("Number2")
-                    )
+                        QuantifiedVariable("Number2"),
+                    ),
                 ),
-                mutableListOf()
+                mutableListOf(),
             ),
-            mutableListOf()
+            mutableListOf(),
         )
 
         e1 = ExistentialQuantifier("C", Not(Relation("Q", listOf(QuantifiedVariable("C")))), mutableListOf())
@@ -112,14 +112,14 @@ class TestFOLogic {
                             "m",
                             listOf(
                                 QuantifiedVariable("X"),
-                                QuantifiedVariable("Y")
-                            )
-                        )
-                    )
+                                QuantifiedVariable("Y"),
+                            ),
+                        ),
+                    ),
                 ),
-                mutableListOf()
+                mutableListOf(),
             ),
-            mutableListOf()
+            mutableListOf(),
         )
         e3 = ExistentialQuantifier(
             "El",
@@ -128,10 +128,10 @@ class TestFOLogic {
                 UniversalQuantifier(
                     "Y",
                     Relation("P", listOf(QuantifiedVariable("Y"))),
-                    mutableListOf()
-                )
+                    mutableListOf(),
+                ),
             ),
-            mutableListOf()
+            mutableListOf(),
         )
     }
 
@@ -181,7 +181,7 @@ class TestFOLogic {
     fun testUnification() {
         val map = Unification.unify(
             Relation("R", listOf(Function("f", listOf(QuantifiedVariable("X"), Function("g", listOf(Constant("c"))))))),
-            Relation("R", listOf(Function("f", listOf(QuantifiedVariable("Y"), QuantifiedVariable("Y")))))
+            Relation("R", listOf(Function("f", listOf(QuantifiedVariable("Y"), QuantifiedVariable("Y"))))),
         )
         val expected = mapOf("X" to Function("g", listOf(Constant("c"))), "Y" to Function("g", listOf(Constant("c"))))
 
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt b/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt
index 52d6556dc..df518452d 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt
@@ -91,8 +91,8 @@ class TestPropositionalLogic {
         val expected3 = ClauseSet(
             mutableListOf(
                 Clause(mutableListOf(Atom("a", true), Atom("c"))),
-                Clause(mutableListOf(Atom("a"), Atom("c")))
-            )
+                Clause(mutableListOf(Atom("a"), Atom("c"))),
+            ),
         )
         assertEquals(expected3.toString(), NaiveCNF.transform(n3).toString())
     }
@@ -104,13 +104,13 @@ class TestPropositionalLogic {
             "{not0}, {!varb, !not3}, {varb, not3}, {!not3, !not2}, {not3, not2}, " +
                 "{not2, !vara, !equiv1}, {!not2, vara, !equiv1}, {!not2, !vara, equiv1}, " +
                 "{not2, vara, equiv1}, {!equiv1, !not0}, {equiv1, not0}",
-            TseytinCNF.transform(n2).toString()
+            TseytinCNF.transform(n2).toString(),
         )
         assertEquals(
             "{not0}, {!vara, !not4}, {vara, not4}, {!vara, or2}, {!not4, or2}, " +
                 "{vara, not4, !or2}, {!varc, !not6}, {varc, not6}, {or2, !and1}, " +
                 "{not6, !and1}, {!or2, !not6, and1}, {!and1, !not0}, {and1, not0}",
-            TseytinCNF.transform(n3).toString()
+            TseytinCNF.transform(n3).toString(),
         )
     }
 
@@ -134,17 +134,17 @@ class TestPropositionalLogic {
             "{and0}, {!vara, !not1}, {vara, not1}, {varb, impl5}, {!vara, impl5}," +
                 " {!varb, vara, !impl5}, {varb, !and3}, {impl5, !and3}, {!varb, !impl5, and3}," +
                 " {not1, !and0}, {and3, !and0}, {!not1, !and3, and0}",
-            TseytinCNF.transform(a1).toString()
+            TseytinCNF.transform(a1).toString(),
         )
         assertEquals(
             "{and0}, {!vara, !not2}, {vara, not2}, {vara, !and0}, {not2, !and0}, " +
                 "{!vara, !not2, and0}",
-            TseytinCNF.transform(a2).toString()
+            TseytinCNF.transform(a2).toString(),
         )
         assertEquals(
             "{and0}, {!vara, !not3}, {vara, not3}, {!vara, or1}, {!not3, or1}, " +
                 "{vara, not3, !or1}, {or1, !and0}, {varb, !and0}, {!or1, !varb, and0}",
-            TseytinCNF.transform(a3).toString()
+            TseytinCNF.transform(a3).toString(),
         )
     }
 
@@ -160,7 +160,7 @@ class TestPropositionalLogic {
         assertEquals("{a, b}", NaiveCNF.transform(o1).toString())
         assertEquals(
             "{a, !b, a, !a}, {a, !b, a, !b}, {a, !b, b, !a}, {a, !b, b, !b}",
-            NaiveCNF.transform(o2).toString()
+            NaiveCNF.transform(o2).toString(),
         )
         assertEquals("{!a, !b, b}, {!a, !b, b}", NaiveCNF.transform(o3).toString())
     }
@@ -169,21 +169,21 @@ class TestPropositionalLogic {
     fun testOrTseytin() {
         assertEquals(
             "{or0}, {!vara, or0}, {!varb, or0}, {vara, varb, !or0}",
-            TseytinCNF.transform(o1).toString()
+            TseytinCNF.transform(o1).toString(),
         )
         assertEquals(
             "{or0}, {!varb, !not3}, {varb, not3}, {!vara, or1}, {!not3, or1}, " +
                 "{vara, not3, !or1}, {vara, !varb, !equiv5}, {!vara, varb, !equiv5}, " +
                 "{!vara, !varb, equiv5}, {vara, varb, equiv5}, {!or1, or0}, " +
                 "{!equiv5, or0}, {or1, equiv5, !or0}",
-            TseytinCNF.transform(o2).toString()
+            TseytinCNF.transform(o2).toString(),
         )
         assertEquals(
             "{or0}, {vara, !and2}, {varb, !and2}, {!vara, !varb, and2}, " +
                 "{!and2, !not1}, {and2, not1}, {!varb, !not8}, {varb, not8}, " +
                 "{varb, impl6}, {!not8, impl6}, {!varb, not8, !impl6}, {!impl6, !not5}, " +
                 "{impl6, not5}, {!not1, or0}, {!not5, or0}, {not1, not5, !or0}",
-            TseytinCNF.transform(o3).toString()
+            TseytinCNF.transform(o3).toString(),
         )
     }
 }
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/TestSyntacticEquality.kt b/backend/src/test/kotlin/kalkulierbar/logic/TestSyntacticEquality.kt
index ec6ea5383..9091d5e63 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/TestSyntacticEquality.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/TestSyntacticEquality.kt
@@ -11,7 +11,7 @@ class TestSyntacticEquality {
     private val equalPairs = listOf(
         Pair("f(g(f(q, a)), c)", "f(g(f(q, a)), c)"),
         Pair("a", "a"),
-        Pair("f(X)", "f(X)")
+        Pair("f(X)", "f(X)"),
     )
 
     private val unequalPairs = listOf(
@@ -20,7 +20,7 @@ class TestSyntacticEquality {
         Pair("f(X, Y)", "f(X, X)"),
         Pair("f(g(f(c)))", "f(g(f(g(c))))"),
         Pair("X", "Y"),
-        Pair("X", "x")
+        Pair("X", "x"),
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestFirstOrderCNF.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestFirstOrderCNF.kt
index ad7e449bd..3412502a7 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestFirstOrderCNF.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestFirstOrderCNF.kt
@@ -13,7 +13,7 @@ class TestFirstOrderCNF {
         "!(R(a) & R(b))" to "{!R(a), !R(b)}",
         "!(!R(a)) <-> !R(a)" to "{R(a), !R(a)}, {R(a), R(a)}, {!R(a), !R(a)}, {!R(a), R(a)}",
         "!\\ex A : \\all B : (R(B) -> !R(A))" to "{R(sk1(A))}, {R(A)}",
-        "!\\all A : \\all C : (R(A) <-> !R(C))" to "{!R(sk1), R(sk2)}, {R(sk1), !R(sk2)}"
+        "!\\all A : \\all C : (R(A) <-> !R(C))" to "{!R(sk1), R(sk2)}, {R(sk1), !R(sk2)}",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNaiveCNF.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNaiveCNF.kt
index 86305eb71..9f04c5692 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNaiveCNF.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNaiveCNF.kt
@@ -16,7 +16,7 @@ class TestNaiveCNF {
         "!(a | b) -> !(!a & b)" to "{a, b, a, !b}",
         "a | !b -> !a <-> b & !a | b" to "{!a, !a, a, !b}, {!a, !a, a}, {!a, !a, !b, a}, {!a, !a, !b}, " +
             "{b, !a, a, !b}, {b, !a, a}, {b, !a, !b, a}, {b, !a, !b}, {b, b, a, !b}, {b, b, a}, " +
-            "{b, b, !b, a}, {b, b, !b}, {!a, b, a, !b}, {!a, b, a}, {!a, b, !b, a}, {!a, b, !b}"
+            "{b, b, !b, a}, {b, b, !b}, {!a, b, a, !b}, {!a, b, a}, {!a, b, !b, a}, {!a, b, !b}",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNegationNormalForm.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNegationNormalForm.kt
index ba6472ac8..c7eb276b2 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNegationNormalForm.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestNegationNormalForm.kt
@@ -13,7 +13,7 @@ class TestNegationNormalForm {
         "!(R(a) & R(b))" to "(¬R(a) ∨ ¬R(b))",
         "!(!R(a))" to "R(a)",
         "!\\ex A : R(A)" to "(∀A: ¬R(A))",
-        "!\\all A : R(A)" to "(∃A: ¬R(A))"
+        "!\\all A : R(A)" to "(∃A: ¬R(A))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestPrenexNormalForm.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestPrenexNormalForm.kt
index 4cc42c989..3e4e4f368 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestPrenexNormalForm.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestPrenexNormalForm.kt
@@ -15,7 +15,7 @@ class TestPrenexNormalForm {
 
         "!\\ex A : !(S(A) & !\\all B : (R(B) -> !R(A)))" to "(∃A: (∀B: ¬¬(S(A) ∧ ¬(R(B) → ¬R(A)))))",
         "!\\all A : (P(A) <-> \\all C : (R(A) <-> !R(C)))" to "(∀A: (∀C: ¬(P(A) <=> (R(A) <=> ¬R(C)))))",
-        "!\\ex A : R(A) -> !\\all B : !(R(B) | !R(B))" to "(∃A: (∀B: (¬R(A) → ¬¬(R(B) ∨ ¬R(B)))))"
+        "!\\ex A : R(A) -> !\\all B : !(R(B) | !R(B))" to "(∃A: (∀B: (¬R(A) → ¬¬(R(B) ∨ ¬R(B)))))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt
index 51ce51fb9..a83d8db5b 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt
@@ -11,22 +11,33 @@ class TestSignature {
         "P(a, g(f(f(f(a))), b, f(c))) & Q(a, b, c)"
             to "Σ(constants={a, b, c}, functions={f(1), g(3)}, relations={P(2), Q(3)}, bound={})",
         "/all X: /all Y: /all Z: (P(X, Y) & P(Y, Z) -> P(X, Z)) & P(a, f(a, a)) & P(f(a, a), g(a, a, a, a))"
-            to "Σ(constants={a}, functions={f(2), g(4)}, relations={P(2)}, bound={X, Y, Z})"
+            to "Σ(constants={a}, functions={f(2), g(4)}, relations={P(2)}, bound={X, Y, Z})",
     )
 
     private val mixedArity = listOf(
         "P(a) & P(a, b)",
         "P(f(a, b), f(c), f(a, b, c))",
         "P(a, a(b))",
-        "P(a(a))"
+        "P(a(a))",
     )
 
     private val sig1 = signature("Σ(constants={a, b, c}, functions={f(1), g(3)}, relations={P(2), Q(3)}, bound={})")
     private val validTerms = listOf(
-        "a", "b", "c", "f(a)", "f(f(b))", "g(f(a), b, g(c, b, f(a)))", "d"
+        "a",
+        "b",
+        "c",
+        "f(a)",
+        "f(f(b))",
+        "g(f(a), b, g(c, b, f(a)))",
+        "d",
     )
     private val invalidTerms = listOf(
-        "a(b)", "f", "f(a, a)", "g(a)", "g(a, b)", "f(g(a, a, b, c))"
+        "a(b)",
+        "f",
+        "f(a, a)",
+        "g(a)",
+        "g(a, b)",
+        "f(g(a, a, b, c))",
     )
 
     private fun compound(s: String): CompoundSignature {
@@ -65,7 +76,8 @@ class TestSignature {
                 assertEquals(signature(expected), csSig)
             } else {
                 assertEquals(
-                    signature(expected), csSig
+                    signature(expected),
+                    csSig,
                 )
             }
         }
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemNormalForm.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemNormalForm.kt
index a4e77c3d6..9eaaaa269 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemNormalForm.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemNormalForm.kt
@@ -17,7 +17,7 @@ class TestSkolemNormalForm {
         "!\\all A : (P(A) <-> \\ex C : (R(A) <-> !R(C)))" to
             "(∀C: ((¬P(sk1) ∨ ((¬R(sk1) ∨ R(C)) ∧ (R(sk1) ∨ ¬R(C)))) ∧ (P(sk1) ∨ " +
             "((R(sk1) ∧ ¬R(sk2)) ∨ (¬R(sk1) ∧ R(sk2))))))",
-        "!\\ex A : R(A) -> !\\all B : !(R(B) | !R(B))" to "(R(sk1) ∨ (R(sk2) ∨ ¬R(sk2)))"
+        "!\\ex A : R(A) -> !\\all B : !(R(B) | !R(B))" to "(R(sk1) ∨ (R(sk2) ∨ ¬R(sk2)))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemization.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemization.kt
index dd1c67478..455f59453 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemization.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSkolemization.kt
@@ -16,7 +16,7 @@ class TestSkolemization {
         "\\ex A: R(A) & Q(sk1)" to "(R(sk2) ∧ Q(sk1))",
         "!\\ex A : !(S(A) & !\\all B : (R(B) -> !R(A)))" to "¬¬(S(sk1) ∧ ¬(∀B: (R(B) → ¬R(sk1))))",
         "!\\all A : (P(A) <-> \\ex C : (R(A) <-> !R(C)))" to "¬(∀A: (P(A) <=> (R(A) <=> ¬R(sk1(A)))))",
-        "!\\ex A : R(A) -> !\\all B : !(R(B) | !R(B))" to "(¬R(sk1) → ¬(∀B: ¬(R(B) ∨ ¬R(B))))"
+        "!\\ex A : R(A) -> !\\all B : !(R(B) | !R(B))" to "(¬R(sk1) → ¬(∀B: ¬(R(B) ∨ ¬R(B))))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestTseytinCNF.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestTseytinCNF.kt
index 10235ac76..bdc42252c 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestTseytinCNF.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestTseytinCNF.kt
@@ -20,7 +20,7 @@ class TestTseytinCNF {
             "{vara, not4, !or2}, {!vara, !not6}, {vara, not6}, {or2, impl1}, {!not6, impl1}, " +
             "{!or2, not6, !impl1}, {!vara, !not11}, {vara, not11}, {varb, !and9}, {not11, !and9}, " +
             "{!varb, !not11, and9}, {!and9, or8}, {!varb, or8}, {and9, varb, !or8}, {impl1, !or8, !equiv0}, " +
-            "{!impl1, or8, !equiv0}, {!impl1, !or8, equiv0}, {impl1, or8, equiv0}"
+            "{!impl1, or8, !equiv0}, {!impl1, !or8, equiv0}, {impl1, or8, equiv0}",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUnification.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUnification.kt
index 2da811980..3913851fe 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUnification.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUnification.kt
@@ -22,7 +22,7 @@ class TestUnification {
         "\\all X: R(X) & \\all Y: R(Y)" to "{X=Y}",
         "\\all X: R(f(g(X))) & \\all Y: R(f(Y))" to "{Y=g(X)}",
         "\\all X: R(f(g(X),X)) & \\all Y: R(f(Y,a))" to "{X=a, Y=g(a)}",
-        "\\all X: R(X) & \\all Y: R(Y)" to "{X=Y}"
+        "\\all X: R(X) & \\all Y: R(Y)" to "{X=Y}",
     )
 
     private val invalid = listOf(
@@ -31,7 +31,7 @@ class TestUnification {
         "R(a) & Q(a)",
         "R(a, c) & R(a,b)",
         "\\all X: \\all Y: (R(f(X)) & R(g(Y)))",
-        "\\all X: (R(f(X)) & R(X))"
+        "\\all X: (R(f(X)) & R(X))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUniqueVariables.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUniqueVariables.kt
index 434aebd65..a1c14aa61 100644
--- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUniqueVariables.kt
+++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestUniqueVariables.kt
@@ -9,7 +9,7 @@ class TestUniqueVariables {
 
     private val formulas = mapOf(
         "\\all X: (R(X) & \\all X: S(X))" to "(∀X: (R(X) ∧ (∀Xv1: S(Xv1))))",
-        "\\all X: R(X) & \\all X: S(X)" to "((∀X: R(X)) ∧ (∀Xv1: S(Xv1)))"
+        "\\all X: R(X) & \\all X: S(X)" to "((∀X: R(X)) ∧ (∀Xv1: S(Xv1)))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestClauseSetParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestClauseSetParser.kt
index b7b81e341..dd8c50f59 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestClauseSetParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestClauseSetParser.kt
@@ -18,7 +18,7 @@ class TestClauseSetParser {
         Pair("a\nb", "{a}, {b}"),
         Pair("a\nb\n", "{a}, {b}"),
         Pair("a; ", "{a}"),
-        Pair("fUnkYvAR;!McVariable,thefirst", "{fUnkYvAR}, {!McVariable, thefirst}")
+        Pair("fUnkYvAR;!McVariable,thefirst", "{fUnkYvAR}, {!McVariable, thefirst}"),
     )
 
     private val validNonGeneric = listOf(
@@ -26,7 +26,7 @@ class TestClauseSetParser {
         Pair("-a", "{!a}"),
         Pair("a|b", "{a}, {b}"),
         Pair("a&b", "{a, b}"),
-        Pair("fUnkYvAR|-McVariable&thefirst", "{fUnkYvAR}, {!McVariable, thefirst}")
+        Pair("fUnkYvAR|-McVariable&thefirst", "{fUnkYvAR}, {!McVariable, thefirst}"),
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestDimacsLikeParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestDimacsLikeParser.kt
index 571a2048d..468e80176 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestDimacsLikeParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestDimacsLikeParser.kt
@@ -18,7 +18,7 @@ class TestDimacsLikeParser {
         Pair("a\n 0 b", "{a}, {b}"),
         Pair("a 0 b 0", "{a}, {b}"),
         Pair("fUnkYvAR 0 -McVariable thefirst", "{fUnkYvAR}, {!McVariable, thefirst}"),
-        Pair("1 -2 0 3", "{1, !2}, {3}")
+        Pair("1 -2 0 3", "{1, !2}, {3}"),
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestFOParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestFOParser.kt
index 2cbe917d4..73b14d563 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestFOParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestFOParser.kt
@@ -26,7 +26,7 @@ class TestFOParser {
         "\\all X: P(\\all: X: P(X))",
         "\\all X: P(Y)",
         "\\all x: P(X)",
-        "\\all X P(X)"
+        "\\all X P(X)",
     )
 
     private val valid = mapOf(
@@ -41,7 +41,7 @@ class TestFOParser {
         "\\ex Xyz: P(Xyz) & \\all X: P(X)" to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X)))",
         "!/ex X: (P(X) <-> !P(X))" to "¬(∃X: (P(X) <=> ¬P(X)))",
         "!(/ex X: (P(X) <-> !P(X)))" to "¬(∃X: (P(X) <=> ¬P(X)))",
-        "/ex Xyz: P(Xyz) & /all X: P(X)" to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X)))"
+        "/ex Xyz: P(Xyz) & /all X: P(X)" to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X)))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt
index cb9ccd741..c4523d22f 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt
@@ -34,7 +34,7 @@ class TestFirstOrderSequentParser {
         "\\all X: P(\\all: X: P(X))",
         "\\all X: P(Y)",
         "\\all x: P(X)",
-        "\\all X P(X)"
+        "\\all X P(X)",
     )
 
     private val valid = mapOf(
@@ -68,7 +68,7 @@ class TestFirstOrderSequentParser {
         "\\ex Xyz: P(Xyz) & \\all X: P(X), P(c) |- /ex Xyz: P(Xyz) & " +
             "/all X: P(X), \\all X: \\all Y: \\all Z: R(m(X, m(Y, Z)), m(m(X,Y), Z))"
             to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X))), P(c) ⊢ ((∃Xyz: P(Xyz)) ∧ (∀X: P(X))), " +
-                "(∀X: (∀Y: (∀Z: R(m(X, m(Y, Z)), m(m(X, Y), Z)))))"
+            "(∀X: (∀Y: (∀Z: R(m(X, m(Y, Z)), m(m(X, Y), Z)))))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestModalLogicParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestModalLogicParser.kt
index c9353085a..9da5e9d56 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestModalLogicParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestModalLogicParser.kt
@@ -22,7 +22,7 @@ class TestModalLogicParser {
         "<->a",
         "<->",
         "(a&b v2",
-        "(a|b"
+        "(a|b",
     )
 
     private val invalidSigned = listOf(
@@ -37,7 +37,7 @@ class TestModalLogicParser {
         "\\sign T: a & b \\sign T: a",
         "a & b \\sign T: a",
         "a & \\sign T: a",
-        "\\sign TF: a"
+        "\\sign TF: a",
     )
 
     private val validSigned = listOf(
@@ -50,7 +50,7 @@ class TestModalLogicParser {
         "\\sign T:      a" to "a",
         "\\sign F:      a" to "a",
         "   \\sign       T: a" to "a",
-        "   \\sign       F: a" to "a"
+        "   \\sign       F: a" to "a",
     )
 
     private val valid = mapOf(
@@ -66,7 +66,7 @@ class TestModalLogicParser {
         "[](a&b)" to "□(a ∧ b)",
         "<>(a&b)" to "◇(a ∧ b)",
         "[]<>(a)" to "□◇a",
-        "[][](a)" to "□□a"
+        "[][](a)" to "□□a",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestPropParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestPropParser.kt
index 8398a6857..50adfd6f2 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestPropParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestPropParser.kt
@@ -20,7 +20,7 @@ class TestPropParser {
         "<->a",
         "<->",
         "(a&b v2",
-        "(a|b"
+        "(a|b",
     )
 
     private val valid = mapOf(
@@ -31,7 +31,7 @@ class TestPropParser {
         "a    ->b" to "(a → b)",
         "a->b" to "(a → b)",
         "a<->(b -> (!(c)))" to "(a <=> (b → ¬c))",
-        "(b & a <-> (a) | !b)" to "((b ∧ a) <=> (a ∨ ¬b))"
+        "(b & a <-> (a) | !b)" to "((b ∧ a) <=> (a ∨ ¬b))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestPropositionalSequentParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestPropositionalSequentParser.kt
index a0514c37f..04afd6305 100644
--- a/backend/src/test/kotlin/kalkulierbar/parsers/TestPropositionalSequentParser.kt
+++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestPropositionalSequentParser.kt
@@ -25,7 +25,7 @@ class TestPropositionalSequentParser {
         "|- a |-",
         "( |- )",
         "a | |- b",
-        "a |- b a"
+        "a |- b a",
     )
 
     private val valid = mapOf(
@@ -53,7 +53,7 @@ class TestPropositionalSequentParser {
         "(b & a <-> (a) | !b)                 |-" to "(((b ∧ a) → (a ∨ ¬b)) ∧ ((a ∨ ¬b) → (b ∧ a))) ⊢ ",
         " |- a,b" to " ⊢ a, b",
         "a,b,c,d,e,f |- g,h,i,j,k,l" to "a, b, c, d, e, f ⊢ g, h, i, j, k, l",
-        "a & b -> c, a | c |- d <-> e" to "((a ∧ b) → c), (a ∨ c) ⊢ ((d → e) ∧ (e → d))"
+        "a & b -> c, a | c |- d <-> e" to "((a ∧ b) → c), (a ∨ c) ⊢ ((d → e) ∧ (e → d))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/propsequent/TestOrRight.kt b/backend/src/test/kotlin/kalkulierbar/propsequent/TestOrRight.kt
index 53a1b9f58..54a1f1a5d 100644
--- a/backend/src/test/kotlin/kalkulierbar/propsequent/TestOrRight.kt
+++ b/backend/src/test/kotlin/kalkulierbar/propsequent/TestOrRight.kt
@@ -30,6 +30,7 @@ class TestOrRight {
         assertTrue(node1.rightFormulas[0] is Var)
         assertTrue(node1.rightFormulas[1] is Var)
     }
+
     @Test
     fun testParent() {
         var state = instance.parseFormulaToState("a | b", null)
diff --git a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue46.kt b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue46.kt
index 8b56b9b07..e64269bac 100644
--- a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue46.kt
+++ b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue46.kt
@@ -11,7 +11,7 @@ class TestIssue46 {
 
     private val testStrings = mapOf(
         "\\all X: Q(X,X) <=> R(c)" to "(((∀X: Q(X, X)) ∧ R(c)) ∨ ((∃Xv1: ¬Q(Xv1, Xv1)) ∧ ¬R(c)))",
-        "\\ex X: \\ex X: R(X, X)" to "(∃X: (∃Xv1: R(Xv1, Xv1)))"
+        "\\ex X: \\ex X: R(X, X)" to "(∃X: (∃Xv1: R(Xv1, Xv1)))",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue48.kt b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue48.kt
index 847504a88..d2147828a 100644
--- a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue48.kt
+++ b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue48.kt
@@ -11,11 +11,11 @@ import kotlin.test.assertFailsWith
 class TestIssue48 {
 
     private val testStrings = mapOf(
-        "\\ex X: R(X) & (R(sk1) <-> R(usk1))" to "(R(sk2) ∧ (R(sk1) <=> R(usk1)))"
+        "\\ex X: R(X) & (R(sk1) <-> R(usk1))" to "(R(sk2) ∧ (R(sk1) <=> R(usk1)))",
     )
 
     private val invalid = listOf(
-        "\\ex X: R(X) & R(sk-1)"
+        "\\ex X: R(X) & R(sk-1)",
     )
 
     @Test
diff --git a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt
index b22418297..a7adaff35 100644
--- a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt
+++ b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt
@@ -17,7 +17,7 @@ class TestIssue50 {
                 "{!In(A_4, M_4), In(A_4, N_4), !Subset(M_4, N_4)}, {!In(A_5, M_5), " +
                 "In(A_5, N_5), In(sk1(M_5, N_5), M_5)}, " +
                 "{!In(A_6, M_6), In(A_6, N_6), !In(sk1(M_6, N_6), N_6)}",
-            state.clauseSet.toString()
+            state.clauseSet.toString(),
         )
     }
 }
diff --git a/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt b/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt
index 398582b0e..b0b27e7ae 100644
--- a/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt
+++ b/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt
@@ -41,28 +41,34 @@ class TestFOResolveUnify {
     @Test
     fun testValid() {
         testFormula(
-            valid1, MoveResolveUnify(0, 1, 0, 0),
-            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3"
+            valid1,
+            MoveResolveUnify(0, 1, 0, 0),
+            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3",
         )
         testFormula(
-            valid2, MoveResolveUnify(0, 1, 0, 0),
-            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3"
+            valid2,
+            MoveResolveUnify(0, 1, 0, 0),
+            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3",
         )
         testFormula(
-            valid3, MoveResolveUnify(0, 1, 0, 0),
-            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(sk1, c), sk1)}, {}||NONE|2|3"
+            valid3,
+            MoveResolveUnify(0, 1, 0, 0),
+            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(sk1, c), sk1)}, {}||NONE|2|3",
         )
         testFormula(
-            valid4, MoveResolveUnify(0, 1, 0, 0),
-            "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4"
+            valid4,
+            MoveResolveUnify(0, 1, 0, 0),
+            "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4",
         )
         testFormula(
-            valid4, MoveResolveUnify(2, 1, 0, 0),
-            "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4"
+            valid4,
+            MoveResolveUnify(2, 1, 0, 0),
+            "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4",
         )
         testFormula(
-            valid5, MoveResolveUnify(2, 1, 1, 0),
-            "resolutionstate|{!R(a), R(c)}, {R(X_2)}, {T(a), !R(f(g(h(a))))}, {T(a)}||NONE|3|4"
+            valid5,
+            MoveResolveUnify(2, 1, 1, 0),
+            "resolutionstate|{!R(a), R(c)}, {R(X_2)}, {T(a), !R(f(g(h(a))))}, {T(a)}||NONE|3|4",
         )
     }
 
@@ -87,12 +93,14 @@ class TestFOResolveUnify {
     @Test
     fun testManual() {
         testFormula(
-            valid1, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "a")),
-            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3"
+            valid1,
+            MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "a")),
+            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3",
         )
         testFormula(
-            valid2, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "Y_2")),
-            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3"
+            valid2,
+            MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "Y_2")),
+            "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3",
         )
         testFormula(valid3, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "f(nope)")))
     }
diff --git a/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt b/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt
index ac28c79b0..38a883fbc 100644
--- a/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt
+++ b/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt
@@ -113,7 +113,7 @@ class TestHyperResolution {
         val state = fo.parseFormulaToState(
             "(S(a) | !S(b) | !S(c) | !S(d)) & (R(b) " +
                 "| R(c)) & (Q(c) | Q(k)) & (P(d) | P(g) | P(h))",
-            null
+            null,
         )
 
         assertFailsWith<IllegalMove> {
@@ -180,14 +180,14 @@ class TestHyperResolution {
         var state = fo.parseFormulaToState(
             "/all X: (R(a) | !R(X) | R(X) | R(d)) & (R(e) " +
                 "| R(f) | R(b) | R(g))",
-            null
+            null,
         )
         state = fo.applyMoveOnState(state, MoveHyper(0, mapOf(1 to Pair(1, 2))))
 
         assertEquals(
             "{R(a), !R(X_1), R(X_1), R(d)}, {R(e), R(f), R(b), R(g)}, " +
                 "{R(a), R(b), R(d), R(e), R(f), R(g)}",
-            state.clauseSet.toString()
+            state.clauseSet.toString(),
         )
     }
 
@@ -197,7 +197,7 @@ class TestHyperResolution {
             "F(a) & !G(a) & /all W:(!F(W) " +
                 "| H(W)) & /all Z:(!J(Z) | !I(Z) | F(Z)) & /all X: /all Y:(!H(X) " +
                 "| G(X) | !H(Y) | !I(Y)) & J(b) & I(b)",
-            null
+            null,
         )
         state = fo.applyMoveOnState(state, MoveHyper(3, mapOf(0 to Pair(5, 0), 1 to Pair(6, 0))))
 
@@ -205,7 +205,7 @@ class TestHyperResolution {
             "{F(a)}, {!G(a)}, {!F(W_3), H(W_3)}, " +
                 "{!J(Z_4), !I(Z_4), F(Z_4)}, {!H(X_5), G(X_5), !H(Y_5), !I(Y_5)}, " +
                 "{J(b)}, {I(b)}, {F(b)}",
-            state.clauseSet.toString()
+            state.clauseSet.toString(),
         )
     }
 }
diff --git a/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt b/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt
index 461f282ff..bd772a1ce 100644
--- a/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt
+++ b/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt
@@ -13,7 +13,7 @@ class TestResolutionJson {
 
     /*
         Test jsonToParam
-    */
+     */
 
     @Test
     fun testJsonParamValid() {
@@ -47,7 +47,7 @@ class TestResolutionJson {
 
     /*
         Test jsonToMove
-    */
+     */
 
     @Test
     fun testJsonMoveValid() {
@@ -106,7 +106,7 @@ class TestResolutionJson {
 
     /*
         Test jsonToState
-    */
+     */
 
     @Test
     fun testJsonState() {
@@ -166,7 +166,7 @@ class TestResolutionJson {
 
     /*
         Test stateToJson
-    */
+     */
 
     @Test
     fun testStateToJson() {
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestAutoCloseBranchFO.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestAutoCloseBranchFO.kt
index 0c21bd710..e23972bc3 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestAutoCloseBranchFO.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestAutoCloseBranchFO.kt
@@ -13,7 +13,7 @@ class TestAutoCloseBranchFO {
         TableauxType.UNCONNECTED,
         regular = false,
         backtracking = false,
-        manualVarAssign = false
+        manualVarAssign = false,
     )
     private var states = mutableListOf<FoTableauxState>()
 
@@ -23,7 +23,7 @@ class TestAutoCloseBranchFO {
         "\\ex A : (R(A) & (\\all B: !R(B) & !R(A)))",
         "\\ex Usk: (R(Usk) -> (!\\ex Usk: (R(sk1) & !R(Usk) | R(Usk) & !R(sk1))))",
         "\\all A: (Sk1(A) -> !\\ex B: (R(A) & !R(B) -> Sk1(B) | !Sk1(A)))",
-        "\\all X: (R(g(X)) & !R(f(X)))"
+        "\\all X: (R(g(X)) & !R(f(X)))",
     )
 
     @BeforeTest
@@ -152,8 +152,8 @@ class TestAutoCloseBranchFO {
         }
     }
 
-    @Test
     // Prints ClauseSet of each state
+    @Test
     fun printStateClauseSet() {
         for (state in states) {
             println(state.clauseSet.toString())
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestCheckClose.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestCheckClose.kt
index d998551e1..994aa7510 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestCheckClose.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestCheckClose.kt
@@ -15,7 +15,7 @@ class TestCheckClose {
 
         val nodes = listOf(
             TableauxNode(0, "a", false),
-            TableauxNode(1, "a", true)
+            TableauxNode(1, "a", true),
         )
 
         state.tree.addAll(nodes)
@@ -39,7 +39,7 @@ class TestCheckClose {
             TableauxNode(0, "a", false),
             TableauxNode(0, "b", false),
             TableauxNode(1, "a", true),
-            TableauxNode(2, "b", true)
+            TableauxNode(2, "b", true),
         )
 
         state.tree.addAll(nodes)
@@ -92,7 +92,7 @@ class TestCheckClose {
             TableauxNode(0, "c", false),
             TableauxNode(1, "a", true),
             TableauxNode(2, "b", true),
-            TableauxNode(3, "c", true)
+            TableauxNode(3, "c", true),
         )
 
         state.tree.addAll(nodes)
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseBranchFO.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseBranchFO.kt
index e68033567..16b2f0a40 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseBranchFO.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseBranchFO.kt
@@ -11,9 +11,10 @@ class TestCloseBranchFO {
     val instance = FirstOrderTableaux()
     private val param = FoTableauxParam(TableauxType.UNCONNECTED, true, backtracking = false, manualVarAssign = true)
     private val paramNotReg = FoTableauxParam(
-        TableauxType.UNCONNECTED, regular = false,
+        TableauxType.UNCONNECTED,
+        regular = false,
         backtracking = false,
-        manualVarAssign = true
+        manualVarAssign = true,
     )
     private var states = mutableListOf<FoTableauxState>()
     private var notRegStates = mutableListOf<FoTableauxState>()
@@ -22,7 +23,7 @@ class TestCloseBranchFO {
         "\\all X: R(X) & R(c) & !R(c)",
         "\\all X: \\ex Y: R(X,Y) & \\ex Z: \\all W: !R(Z, W)", // R(X, sk1(X)), !R(sk2, W)
         "\\all A: (\\all B: (R(A) -> R(B) & !R(A) | !R(B)))",
-        "\\all A: (R(A) -> !\\ex B: (R(A) & !R(B) -> R(B) | R(A)))"
+        "\\all A: (R(A) -> !\\ex B: (R(A) & !R(B) -> R(B) | R(A)))",
     )
 
     @BeforeTest
@@ -117,8 +118,8 @@ class TestCloseBranchFO {
         assertEquals(state.tree[6].closeRef, 2)
     }
 
-    @Test
     // Prints ClauseSet of each state
+    @Test
     fun printStateClauseSet() {
         for (state in states) {
             println(state.clauseSet.toString())
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseLeaf.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseLeaf.kt
index dba183269..9dc848274 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseLeaf.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestCloseLeaf.kt
@@ -17,7 +17,7 @@ class TestCloseLeaf {
         val nodes = listOf(
             TableauxNode(0, "a", false),
             TableauxNode(0, "b", false),
-            TableauxNode(2, "b", true)
+            TableauxNode(2, "b", true),
         )
         state = createArtificialExpandState(nodes, state)
         state = instance.applyMoveOnState(state, MoveAutoClose(3, 2))
@@ -27,7 +27,7 @@ class TestCloseLeaf {
         assertEquals(
             "tableauxstate|UNCONNECTED|false|false|false|{a, b}, {!b}|" +
                 "[true;p;null;-;i;o;(1,2)|a;p;0;-;l;o;()|b;p;0;-;i;c;(3)|b;n;2;2;l;c;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -39,7 +39,7 @@ class TestCloseLeaf {
             TableauxNode(0, "b", true),
             TableauxNode(1, "a", false),
             TableauxNode(1, "b", false),
-            TableauxNode(1, "c", false)
+            TableauxNode(1, "c", false),
         )
         state = createArtificialExpandState(nodes, state)
         state = instance.applyMoveOnState(state, MoveAutoClose(3, 1))
@@ -54,7 +54,7 @@ class TestCloseLeaf {
             "tableauxstate|UNCONNECTED|false|false|false|{a, b, c}, {!a}, {!b}, {!c}|" +
                 "[true;p;null;-;i;o;(1)|b;n;0;-;i;o;(2,3,4)|a;p;1;-;l;o;()|" +
                 "b;p;1;1;l;c;()|c;p;1;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -67,7 +67,7 @@ class TestCloseLeaf {
             TableauxNode(0, "b", false),
             TableauxNode(0, "c", false),
             TableauxNode(1, "a", true),
-            TableauxNode(2, "b", true)
+            TableauxNode(2, "b", true),
         )
         state = createArtificialExpandState(nodes, state)
 
@@ -85,7 +85,7 @@ class TestCloseLeaf {
             "tableauxstate|UNCONNECTED|false|false|false|{a, b, c}, {!a}, {!b}, {!c}|" +
                 "[true;p;null;-;i;o;(1,2,3)|a;p;0;-;i;c;(4)|b;p;0;-;i;c;(5)|c;p;0;-;l;o;()|a;n;1;1;l;c;()|" +
                 "b;n;2;2;l;c;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -114,7 +114,7 @@ class TestCloseLeaf {
             TableauxNode(0, "a", false),
             TableauxNode(0, "b", false),
             TableauxNode(1, "a", false),
-            TableauxNode(1, "b", false)
+            TableauxNode(1, "b", false),
         )
         state = createArtificialExpandState(nodes, state)
 
@@ -137,7 +137,7 @@ class TestCloseLeaf {
 
         val nodes = listOf(
             TableauxNode(0, "c", false),
-            TableauxNode(1, "c", false)
+            TableauxNode(1, "c", false),
         )
         state = createArtificialExpandState(nodes, state)
 
@@ -165,7 +165,7 @@ class TestCloseLeaf {
             TableauxNode(1, "b", false),
             TableauxNode(2, "b", true),
             TableauxNode(5, "a", false),
-            TableauxNode(5, "b", false)
+            TableauxNode(5, "b", false),
         )
         state = createArtificialExpandState(nodes, state)
 
@@ -188,7 +188,7 @@ class TestCloseLeaf {
 
         val nodes = listOf(
             TableauxNode(0, "c", false),
-            TableauxNode(1, "c", true)
+            TableauxNode(1, "c", true),
         )
         state = createArtificialExpandState(nodes, state)
         state = instance.applyMoveOnState(state, MoveAutoClose(2, 1))
@@ -204,7 +204,7 @@ class TestCloseLeaf {
 
         val nodes = listOf(
             TableauxNode(0, "a", false),
-            TableauxNode(1, "c", true)
+            TableauxNode(1, "c", true),
         )
         state = createArtificialExpandState(nodes, state)
 
@@ -218,7 +218,7 @@ class TestCloseLeaf {
         var state = instance.parseFormulaToState("!true", opts)
 
         val nodes = listOf(
-            TableauxNode(0, "true", true)
+            TableauxNode(0, "true", true),
         )
         state = createArtificialExpandState(nodes, state)
 
@@ -238,7 +238,7 @@ class TestCloseLeaf {
             TableauxNode(1, "a", false),
             TableauxNode(2, "b", true),
             TableauxNode(5, "a", true),
-            TableauxNode(5, "b", false)
+            TableauxNode(5, "b", false),
         )
         state = createArtificialExpandState(nodes, state)
 
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectedness.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectedness.kt
index 54ac3ea90..d6e8c1bd6 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectedness.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectedness.kt
@@ -29,7 +29,7 @@ class TestConnectedness {
             "tableauxstate|WEAKLYCONNECTED|false|false|false|{a, b, c}, {!a, b}|" +
                 "[true;p;null;-;i;o;(1,2,3)|a;p;0;-;i;o;(4,5)|b;p;0;-;l;o;()|c;p;0;-;l;o;()|a;n;1;1;l;c;()|" +
                 "b;p;1;-;i;o;(6,7)|a;n;5;1;l;c;()|b;p;5;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -49,7 +49,7 @@ class TestConnectedness {
         assertEquals(
             "tableauxstate|WEAKLYCONNECTED|false|false|false|{!a, b}, {a}|[true;p;null;-;i;o;(1)|" +
                 "a;p;0;-;i;o;(2,3)|a;n;1;1;l;c;()|b;p;1;-;i;o;(4,5)|a;n;3;1;l;c;()|b;p;3;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -72,7 +72,7 @@ class TestConnectedness {
             "tableauxstate|STRONGLYCONNECTED|false|false|false|{a, b, c}, {!a, b}|" +
                 "[true;p;null;-;i;o;(1,2,3)|a;p;0;-;i;o;(4,5)|b;p;0;-;l;o;()|c;p;0;-;l;o;()|a;n;1;1;l;c;()|" +
                 "b;p;1;-;i;o;(6,7)|a;n;5;-;l;o;()|b;p;5;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -94,7 +94,7 @@ class TestConnectedness {
         assertEquals(
             "tableauxstate|STRONGLYCONNECTED|false|false|false|{!a, b}, {a}|[true;p;null;-;i;o;(1)|" +
                 "a;p;0;-;i;o;(2,3)|a;n;1;1;l;c;()|b;p;1;-;i;o;(4,5)|a;n;3;-;l;o;()|b;p;3;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -117,7 +117,7 @@ class TestConnectedness {
         assertEquals(
             "tableauxstate|WEAKLYCONNECTED|false|false|false|{!a, b}, {a}|[true;p;null;-;i;o;(1)|" +
                 "a;p;0;-;i;o;(2,3)|a;n;1;1;l;c;()|b;p;1;-;i;o;(4,5)|a;n;3;-;l;o;()|b;p;3;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -136,7 +136,7 @@ class TestConnectedness {
             "tableauxstate|STRONGLYCONNECTED|false|false|false|{!a, b}, {a}|" +
                 "[true;p;null;-;i;o;(1,2)|a;n;0;-;i;o;(3,4)|b;p;0;-;l;o;()|a;n;1;-;l;o;()|" +
                 "b;p;1;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 }
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectednessFO.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectednessFO.kt
index 09e98fb17..5b445e166 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectednessFO.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestConnectednessFO.kt
@@ -11,18 +11,18 @@ class TestConnectednessFO {
         TableauxType.WEAKLYCONNECTED,
         regular = false,
         backtracking = true,
-        manualVarAssign = false
+        manualVarAssign = false,
     )
     private val strong = FoTableauxParam(
         TableauxType.STRONGLYCONNECTED,
         regular = false,
         backtracking = true,
-        manualVarAssign = false
+        manualVarAssign = false,
     )
 
     /*
         Test strong connectedness
-    */
+     */
 
     @Test
     fun testValidStrongProof() {
@@ -47,7 +47,7 @@ class TestConnectednessFO {
 
     /*
         Test weak connectedness
-    */
+     */
 
     @Test
     fun testValidWeakProof() {
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestExpandLeaf.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestExpandLeaf.kt
index 9a1304b4d..163fb19db 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestExpandLeaf.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestExpandLeaf.kt
@@ -16,7 +16,7 @@ class TestExpandLeaf {
         val state = instance.parseFormula(
             "a,b;c",
             "{\"type\":\"UNCONNECTED\",\"regular\":" +
-                "false,\"backtracking\":false}"
+                "false,\"backtracking\":false}",
         )
 
         assertFailsWith<JsonParseException> {
@@ -44,7 +44,7 @@ class TestExpandLeaf {
         assertEquals(
             "tableauxstate|UNCONNECTED|false|false|false|{a, b, c}, {d}|[true;p;null;-;i;o;(1,2,3)|" +
                 "a;p;0;-;l;o;()|b;p;0;-;l;o;()|c;p;0;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -60,7 +60,7 @@ class TestExpandLeaf {
         assertEquals(
             "tableauxstate|UNCONNECTED|false|false|false|{a, b, c}, {d}|[true;p;null;-;i;o;(1)|" +
                 "d;p;0;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -79,7 +79,7 @@ class TestExpandLeaf {
             "tableauxstate|UNCONNECTED|false|false|false|{a, b, c}, {d}|" +
                 "[true;p;null;-;i;o;(1,2,3)|a;p;0;-;l;o;()|b;p;0;-;l;o;()|c;p;0;-;i;o;(4)|" +
                 "d;p;3;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestFOLemma.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestFOLemma.kt
index 69d754b2f..f1db2b274 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestFOLemma.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestFOLemma.kt
@@ -13,13 +13,13 @@ class TestFOLemma {
         TableauxType.UNCONNECTED,
         regular = false,
         backtracking = false,
-        manualVarAssign = false
+        manualVarAssign = false,
     )
     private val manualParam = FoTableauxParam(
         TableauxType.UNCONNECTED,
         regular = false,
         backtracking = false,
-        manualVarAssign = true
+        manualVarAssign = true,
     )
 
     private var autoStates = mutableListOf<FoTableauxState>()
@@ -27,7 +27,7 @@ class TestFOLemma {
 
     val formula = listOf(
         "\\all A: (\\all B: (R(A) -> R(B) & !R(A) | !R(B)))",
-        "\\all A: (R(A) -> !\\ex B: (R(A) & !R(B) -> R(B) & R(A)))"
+        "\\all A: (R(A) -> !\\ex B: (R(A) & !R(B) -> R(B) & R(A)))",
     )
 
     @BeforeTest
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt
index bf541eec8..1f084234c 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt
@@ -11,7 +11,7 @@ class TestFirstOrderJson {
 
     /*
         Test jsonToMove
-    */
+     */
 
     @Test
     fun testJsonMoveValid() {
@@ -46,7 +46,7 @@ class TestFirstOrderJson {
 
     /*
         Test jsonToState
-    */
+     */
 
     @Test
     fun testJsonStateEmpty() {
@@ -93,7 +93,7 @@ class TestFirstOrderJson {
 
     /*
         Test stateToJson
-    */
+     */
 
     @Test
     fun testStateToJson() {
@@ -115,7 +115,7 @@ class TestFirstOrderJson {
 
     /*
         Test jsonToParam
-    */
+     */
 
     @Test
     fun testJsonParamValid() {
@@ -126,9 +126,9 @@ class TestFirstOrderJson {
                 TableauxType.UNCONNECTED,
                 regular = false,
                 backtracking = false,
-                manualVarAssign = true
+                manualVarAssign = true,
             ),
-            param
+            param,
         )
     }
 
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestLemma.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestLemma.kt
index c88c6b4c6..0427ca9d6 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestLemma.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestLemma.kt
@@ -16,7 +16,7 @@ class TestLemma {
         "a,a;!a,b;!b",
         "a;b,b;!a,!b",
         "!a,b;!b;a,b",
-        "a,b;!b;!a,b"
+        "a,b;!b;!a,b",
     )
 
     @BeforeTest
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt
index 58fba8d11..461a1c3f1 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt
@@ -11,7 +11,7 @@ class TestPropositionalJson {
 
     /*
         Test jsonToMove
-    */
+     */
 
     @Test
     fun testJsonMoveValid() {
@@ -46,7 +46,7 @@ class TestPropositionalJson {
 
     /*
         Test jsonToState
-    */
+     */
 
     @Test
     fun testJsonStateEmpty() {
@@ -64,7 +64,7 @@ class TestPropositionalJson {
         assertEquals(
             "tableauxstate|UNCONNECTED|false|false|false|{a, b}, {!a}, {!b}|" +
                 "[true;p;null;-;l;o;()]|[]",
-            state.getHash()
+            state.getHash(),
         )
     }
 
@@ -139,7 +139,7 @@ class TestPropositionalJson {
 
     /*
         Test jsonToParam
-    */
+     */
 
     @Test
     fun testJsonParamValid() {
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestRegularity.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestRegularity.kt
index 3e917e643..d792ac50e 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestRegularity.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestRegularity.kt
@@ -28,7 +28,7 @@ class TestRegularity {
             TableauxNode(0, "a", false),
             TableauxNode(0, "b", false),
             TableauxNode(2, "b", true),
-            TableauxNode(1, "a", true)
+            TableauxNode(1, "a", true),
         )
 
         state = createState(nodes, state)
@@ -45,7 +45,7 @@ class TestRegularity {
             TableauxNode(0, "b", false),
             TableauxNode(1, "a", true),
             TableauxNode(2, "b", true),
-            TableauxNode(4, "a", false)
+            TableauxNode(4, "a", false),
         )
 
         state = createState(nodes, state)
@@ -60,7 +60,7 @@ class TestRegularity {
         val nodes = listOf(
             TableauxNode(0, "true", false),
             TableauxNode(0, "false", false),
-            TableauxNode(1, "true", true)
+            TableauxNode(1, "true", true),
         )
 
         state = createState(nodes, state)
@@ -87,7 +87,7 @@ class TestRegularity {
 
         val nodes = listOf(
             TableauxNode(0, "a", false),
-            TableauxNode(1, "a", false)
+            TableauxNode(1, "a", false),
         )
 
         state = createState(nodes, state)
@@ -103,7 +103,7 @@ class TestRegularity {
             TableauxNode(0, "a", false),
             TableauxNode(1, "a", true),
             TableauxNode(2, "b", false),
-            TableauxNode(3, "a", false)
+            TableauxNode(3, "a", false),
         )
 
         state = createState(nodes, state)
@@ -120,7 +120,7 @@ class TestRegularity {
             TableauxNode(0, "b", false),
             TableauxNode(1, "b", false),
             TableauxNode(2, "a", false),
-            TableauxNode(2, "b", false)
+            TableauxNode(2, "b", false),
         )
 
         state = createState(nodes, state)
@@ -135,7 +135,7 @@ class TestRegularity {
         val nodes = listOf(
             TableauxNode(0, "true", false),
             TableauxNode(1, "true", true),
-            TableauxNode(2, "true", false)
+            TableauxNode(2, "true", false),
         )
 
         state = createState(nodes, state)
diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt
index 3107c6ecd..39324746d 100644
--- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt
+++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt
@@ -11,13 +11,13 @@ class TestUndoFO {
         TableauxType.UNCONNECTED,
         regular = false,
         backtracking = true,
-        manualVarAssign = false
+        manualVarAssign = false,
     )
     private val paramManual = FoTableauxParam(
         TableauxType.UNCONNECTED,
         regular = false,
         backtracking = true,
-        manualVarAssign = true
+        manualVarAssign = true,
     )
     private var states = mutableListOf<FoTableauxState>()
     private var statesManual = mutableListOf<FoTableauxState>()
@@ -25,7 +25,7 @@ class TestUndoFO {
     val formula = mutableListOf(
         "\\all X: R(X) & R(c) & !R(c)",
         "\\all A: (\\all B: (R(A) -> R(B) & !R(A) | !R(B)))",
-        "\\all A: (R(A) -> !\\ex B: (R(A) & !R(B) -> R(B) | R(A)))"
+        "\\all A: (R(A) -> !\\ex B: (R(A) & !R(B) -> R(B) | R(A)))",
     )
 
     @BeforeTest