4 files changed, 0 insertions, 74 deletions
diff --git a/test/golden/indefinite-terms/encoding tasks.golden b/test/golden/indefinite-terms/encoding tasks.golden
deleted file mode 100644
index 60bf285..0000000
--- a/test/golden/indefinite-terms/encoding tasks.golden
+++ /dev/null
@@ -1,4 +0,0 @@
-fof(zf_q0,conjecture,$true).
-------------------
-fof(zf_q0,conjecture,$true).
-fof(zf_h0,axiom,$true).
-\ No newline at end of file
diff --git a/test/golden/indefinite-terms/generating tasks.golden b/test/golden/indefinite-terms/generating tasks.golden
deleted file mode 100644
index 6cebfc4..0000000
--- a/test/golden/indefinite-terms/generating tasks.golden
+++ /dev/null
@@ -1,28 +0,0 @@
-[ Task
-    { taskDirectness = Direct
-    , taskHypotheses = []
-    , taskConjectureLabel = Marker "indefinite_test_forall"
-    , taskLocation = Location
-        { locFile = "test/examples/indefinite-terms.tex"
-        , locLine = 1
-        , locColumn = 1
-        }
-    , taskConjecture = PropositionalConstant IsTop
-    }
-, Task
-    { taskDirectness = Direct
-    , taskHypotheses =
-        [ Hypothesis Marker "indefinite_test_forall" Quantified Universally
-            ( Scope
-                ( Connected Implication ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) )
-            )
-        ]
-    , taskConjectureLabel = Marker "indefinite_test_exists"
-    , taskLocation = Location
-        { locFile = "test/examples/indefinite-terms.tex"
-        , locLine = 5
-        , locColumn = 1
-        }
-    , taskConjecture = PropositionalConstant IsTop
-    }
-]
-\ No newline at end of file
diff --git a/test/golden/indefinite-terms/glossing.golden b/test/golden/indefinite-terms/glossing.golden
deleted file mode 100644
index 3cab448..0000000
--- a/test/golden/indefinite-terms/glossing.golden
+++ /dev/null
@@ -1,31 +0,0 @@
-[ BlockLemma
-    ( Location
-        { locFile = "test/examples/indefinite-terms.tex"
-        , locLine = 1
-        , locColumn = 1
-        }
-    )
-    ( Marker "indefinite_test_forall" )
-    ( Lemma []
-        ( Quantified Universally
-            ( Scope
-                ( Connected Implication ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) )
-            )
-        )
-    )
-, BlockLemma
-    ( Location
-        { locFile = "test/examples/indefinite-terms.tex"
-        , locLine = 5
-        , locColumn = 1
-        }
-    )
-    ( Marker "indefinite_test_exists" )
-    ( Lemma []
-        ( Quantified Existentially
-            ( Scope
-                ( Connected Conjunction ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) )
-            )
-        )
-    )
-]
-\ No newline at end of file
diff --git a/test/golden/indefinite-terms/verification.golden b/test/golden/indefinite-terms/verification.golden
deleted file mode 100644
index d13aa99..0000000
--- a/test/golden/indefinite-terms/verification.golden
+++ /dev/null
@@ -1,11 +0,0 @@
-VerifiedWithTrustedVampire
-    ( VerificationReport
-        { verificationRoute = LegacyVerificationRoute
-        , verificationLegacyDeclaredAssumptionCount = 0
-        , verificationTypedDeclaredAssumptionCount = 0
-        , verificationTrustedVampireCount = 2
-        , verificationExplicitGapLocations = []
-        , verificationTrustedLegacyRuleCount = 2
-        , verificationKernelProofCount = 0
-        }
-    )
-\ No newline at end of file