diff --git a/include/PetriEngine/AbstractPetriNetBuilder.h b/include/PetriEngine/AbstractPetriNetBuilder.h
index 966a00a27..de275e60a 100644
--- a/include/PetriEngine/AbstractPetriNetBuilder.h
+++ b/include/PetriEngine/AbstractPetriNetBuilder.h
@@ -105,6 +105,11 @@ namespace PetriEngine {
             throw base_error("Product colors are not supported in standard P/T nets");
         }
 
+        virtual void addTokens(std::string&& place, Colored::Multiset&& tokens)
+        {
+            throw base_error("Parsing marking is not supported");
+        }
+
         virtual void enableColors() {
             _isColored = true;
         }
diff --git a/include/PetriEngine/Colored/ColoredPetriNetBuilder.h b/include/PetriEngine/Colored/ColoredPetriNetBuilder.h
index 4a70e5c65..906130a21 100644
--- a/include/PetriEngine/Colored/ColoredPetriNetBuilder.h
+++ b/include/PetriEngine/Colored/ColoredPetriNetBuilder.h
@@ -152,6 +152,13 @@ namespace PetriEngine {
             return _string_set;
         }
 
+        // Since ColoredPetriNetBuilder takes ownership of any colors given to it, we need to be able to tell it to
+        // forget about those colors and "leak" the memory
+        void leak_colors()
+        {
+            _ownsColors = false;
+        }
+
     private:
         shared_name_index_map _placenames;
         shared_name_index_map _transitionnames;
@@ -164,6 +171,7 @@ namespace PetriEngine {
         Colored::ColorTypeMap _colors;
         PetriNetBuilder _ptBuilder;
         shared_string_set& _string_set;
+        bool _ownsColors = true;
 
         void addArc(const std::string& place,
                 const std::string& transition,
diff --git a/include/PetriEngine/Colored/PnmlWriter.h b/include/PetriEngine/Colored/PnmlWriter.h
index 426caed5a..3a756e519 100644
--- a/include/PetriEngine/Colored/PnmlWriter.h
+++ b/include/PetriEngine/Colored/PnmlWriter.h
@@ -11,10 +11,23 @@
 namespace PetriEngine::Colored {
     class PnmlWriter {
     public:
-        PnmlWriter(PetriEngine::ColoredPetriNetBuilder &b, std::ostream &out) : _builder(b), _out(out), _tabsCount(0) {}
+        PnmlWriter(PetriEngine::ColoredPetriNetBuilder &b, std::ostream &out) : _builder(b), _out(out), _tabsCount(0)
+        {
+            for (auto &namedSort: _builder._colors)
+            {
+                std::vector<const ColorType *> types;
+                ColorType *colortype = const_cast<ColorType *>(namedSort.second);
+                colortype->getColortypes(types);
+                if (is_number(types[0]->operator[](size_t{0}).getColorName())) {
+                    _namedSortTypes.emplace(colortype->getName(), "finite range");
+                } else {
+                    _namedSortTypes.emplace(colortype->getName(), "cyclic enumeration");
+                }
+            }
+        }
 
         void toColPNML();
-
+        void writeInitialTokens(const std::string& placeId);
     private:
         PetriEngine::ColoredPetriNetBuilder &_builder;
         std::ostream &_out;
@@ -77,6 +90,8 @@ namespace PetriEngine::Colored {
 
         void handlehlinitialMarking(Multiset marking);
 
+        void handleTokenExpression(const Multiset& tokens);
+
         void handleType(const Place &place);
 
         void add_arcs_from_transition(Transition &transition);
diff --git a/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h b/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h
index 79ab674c9..bffe1a1c8 100644
--- a/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h
+++ b/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h
@@ -2,6 +2,7 @@
 #define COLORED_RESULT_PRINTER_H
 
 #include "AtomicTypes.h"
+#include "ExplicitColoredPetriNetBuilder.h"
 #include "PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h"
 #include "PetriEngine/Reachability/ReachabilityResult.h"
 
@@ -28,12 +29,22 @@ namespace PetriEngine::ExplicitColored {
         bool isInitial;
     };
 
+    struct ExplicitColoredTraceContext
+    {
+        ExplicitColoredTraceContext(std::vector<TraceStep> traceSteps, ExplicitColoredPetriNetBuilder cpnBuilder)
+            : traceSteps(std::move(traceSteps)), cpnBuilder(std::move(cpnBuilder)) {}
+        ExplicitColoredTraceContext(ExplicitColoredTraceContext&&) = default;
+        ExplicitColoredTraceContext& operator=(ExplicitColoredTraceContext&&) = default;
+        std::vector<TraceStep> traceSteps;
+        ExplicitColoredPetriNetBuilder cpnBuilder;
+    };
+
     class IColoredResultPrinter {
     public:
         virtual void printResult(
             const SearchStatistics& searchStatistics,
             Reachability::AbstractHandler::Result result,
-            const std::vector<TraceStep>* trace
+            const ExplicitColoredTraceContext* trace
         ) const = 0;
         virtual void printNonExplicitResult(
             std::vector<std::string> techniques,
@@ -58,7 +69,7 @@ namespace PetriEngine::ExplicitColored {
         void printResult(
             const SearchStatistics& searchStatistics,
             Reachability::AbstractHandler::Result result,
-            const std::vector<TraceStep>* trace
+            const ExplicitColoredTraceContext* trace
         ) const override;
 
         void printNonExplicitResult(
@@ -67,7 +78,8 @@ namespace PetriEngine::ExplicitColored {
         ) const override;
     private:
         void _printCommon(Reachability::AbstractHandler::Result result, const std::vector<std::string>& extraTechniques) const;
-        void _printTrace(const std::vector<TraceStep>& trace) const;
+        void _printTrace(const ExplicitColoredTraceContext& trace) const;
+        void _printMarkings(const ExplicitColoredPetriNetBuilder& explicitCpnBuilder, const TraceStep& traceStep) const;
         uint32_t _queryOffset;
         std::ostream& _stream;
         std::string _queryName;
diff --git a/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h b/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h
index 18ced1178..de9439cfc 100644
--- a/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h
+++ b/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h
@@ -12,17 +12,17 @@ namespace PetriEngine::ExplicitColored {
     public:
         static int run(const std::string& model_path);
     private:
-        ExplicitColoredInteractiveMode(const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, const ExplicitColoredPetriNetBuilder& builder);
+        ExplicitColoredInteractiveMode(const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, ExplicitColoredPetriNetBuilder& builder);
         int _run_internal();
         static std::string _readUntilDoubleNewline(std::istream& in);
-        std::optional<ColoredPetriNetMarking> _parseMarking(const rapidxml::xml_document<>& markingXml, std::ostream& errorOut) const;
+        std::optional<ColoredPetriNetMarking> _parseMarking(const rapidxml::xml_document<>& markingXml, std::ostream& errorOut);
         std::optional<std::pair<Transition_t, Binding>> _parseTransition(const rapidxml::xml_document<>& transitionXml, std::ostream& errorOut) const;
         void _printCurrentMarking(std::ostream& out, const ColoredPetriNetMarking& currentMarking) const;
         void _printValidBindings(std::ostream& out, const ColoredPetriNetMarking& currentMarking) const;
         std::optional<Color_t> _findColorIndex(const Colored::ColorType* colorType, const char* colorName) const;
         const ColoredSuccessorGenerator& _successorGenerator;
         const ColoredPetriNet& _cpn;
-        const ExplicitColoredPetriNetBuilder& _builder;
+        ExplicitColoredPetriNetBuilder& _builder;
     };
 }
 #endif //COLOREDINTERACTIVEMODE_H
diff --git a/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h b/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h
index 8b3564e4e..1a8d226d1 100644
--- a/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h
+++ b/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h
@@ -7,6 +7,7 @@
 #include "Visitors/ConditionCopyVisitor.h"
 
 #include "ColoredResultPrinter.h"
+#include "ExplicitColoredPetriNetBuilder.h"
 #include "Algorithms/ExplicitWorklist.h"
 
 namespace PetriEngine::ExplicitColored {
@@ -34,7 +35,7 @@ namespace PetriEngine::ExplicitColored {
             options_t& options
         ) const;
 
-        std::pair<Result, std::optional<std::vector<TraceStep>>> explicitColorCheck(
+        std::pair<Result, std::optional<ExplicitColoredTraceContext>> explicitColorCheck(
             const std::string& pnmlModel,
             const PQL::Condition_ptr& query,
             options_t& options,
diff --git a/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h b/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h
index e9d0c28ab..c8caba042 100644
--- a/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h
+++ b/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h
@@ -1,5 +1,7 @@
 #ifndef EXPLICIT_COLORED_PETRI_NET_BUILDER_H
 #define EXPLICIT_COLORED_PETRI_NET_BUILDER_H
+#include <rapidxml.hpp>
+
 #include "PetriEngine/AbstractPetriNetBuilder.h"
 #include "ColoredPetriNet.h"
 
@@ -27,6 +29,7 @@ namespace PetriEngine::ExplicitColored {
         void addColorType(const std::string& id, const Colored::ColorType* type) override;
         void addVariable(const Colored::Variable* variable) override;
         void addToColorType(Colored::ProductType* colorType, const Colored::ColorType* newConstituent) override;
+        void addTokens(std::string&& place, Colored::Multiset&& tokens) override;
         void sort() override;
 
         const std::unordered_map<std::string, uint32_t>& getPlaceIndices() const;
@@ -45,6 +48,8 @@ namespace PetriEngine::ExplicitColored {
 
         ColoredPetriNetBuilderStatus build();
         ColoredPetriNet takeNet();
+
+        ColoredPetriNetMarking parseMarking(const rapidxml::xml_document<>& markingXml);
     private:
         std::unordered_map<Place_t, const Colored::ColorType*> _underlyingColorType;
         std::unordered_map<std::string, Place_t> _placeIndices;
@@ -66,6 +71,8 @@ namespace PetriEngine::ExplicitColored {
         std::unordered_map<Transition_t, std::string> _transitionToId;
         std::unordered_map<Variable_t, std::string> _variableToId;
 
+        bool _parsingStandAloneMarking = false;
+        ColoredPetriNetMarking _standAloneMarking;
         void _createArcsAndTransitions();
         ColoredPetriNetBuilderStatus _calculateTransitionVariables();
         void _calculatePrePlaceConstraints();
diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h
index f9f56535e..fa29e27fe 100644
--- a/include/PetriEngine/PQL/Contexts.h
+++ b/include/PetriEngine/PQL/Contexts.h
@@ -36,6 +36,8 @@
 #include <chrono>
 #include <glpk.h>
 
+#include <chrono>
+
 namespace PetriEngine {
 
     namespace PQL {
@@ -179,9 +181,9 @@ namespace PetriEngine {
         public:
 
             SimplificationContext(const MarkVal* marking,
-                    const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
+                    const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, uint32_t lpPrintLevel,
                     Simplification::LPCache* cache, uint32_t potencyTimeout = 0)
-                    : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout),
+                    : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), _lpPrintLevel(lpPrintLevel),
                     _potencyTimeout(potencyTimeout) {
                 _negated = false;
                 _marking = marking;
@@ -195,8 +197,12 @@ namespace PetriEngine {
                         _markingOutOfBounds = true;
                     }
                 }
+
+                _id = std::chrono::system_clock::now();
             }
 
+            std::chrono::time_point<std::chrono::system_clock> _id;
+
             virtual ~SimplificationContext() {
                 if(_base_lp != nullptr)
                     glp_delete_prob(_base_lp);
@@ -244,6 +250,7 @@ namespace PetriEngine {
 
             uint32_t getLpTimeout() const;
             uint32_t getPotencyTimeout() const;
+            uint32_t getPrintLevel() const;
 
             Simplification::LPCache* cache() const
             {
@@ -257,7 +264,7 @@ namespace PetriEngine {
             const MarkVal* _marking;
             bool _markingOutOfBounds;
             const PetriNet* _net;
-            uint32_t _queryTimeout, _lpTimeout, _potencyTimeout;
+            uint32_t _queryTimeout, _lpTimeout, _lpPrintLevel, _potencyTimeout;
             mutable glp_prob* _base_lp = nullptr;
             std::chrono::high_resolution_clock::time_point _start;
             Simplification::LPCache* _cache;
diff --git a/include/PetriEngine/PQL/Simplifier.h b/include/PetriEngine/PQL/Simplifier.h
index d96e8e3ff..9ca81c469 100644
--- a/include/PetriEngine/PQL/Simplifier.h
+++ b/include/PetriEngine/PQL/Simplifier.h
@@ -39,6 +39,13 @@ namespace PetriEngine { namespace PQL {
         SimplificationContext& _context;
         Retval _return_value;
 
+        enum LPQUANT {NONE, GLOBAL, FINAL, OTHER, UNTIL};
+        LPQUANT quantifier_found = LPQUANT::NONE;
+        LPQUANT quantifier_parent = LPQUANT::NONE;
+        bool qparent_neg_context = false;
+        int32_t quantifiers = 0;
+      
+
         Retval simplify_or(const LogicalCondition* element);
         Retval simplify_and(const LogicalCondition *element);
 
@@ -50,6 +57,8 @@ namespace PetriEngine { namespace PQL {
         Retval simplify_EF(Retval &r);
         Retval simplify_EX(Retval &r);
 
+        Retval simplify_global_quantifier(Retval &r);
+
         template <typename Quantifier>
         Retval simplify_simple_quantifier(Retval &r);
 
diff --git a/include/PetriEngine/Simplification/LinearPrograms.h b/include/PetriEngine/Simplification/LinearPrograms.h
index 0b222ebf6..c96ce1c78 100644
--- a/include/PetriEngine/Simplification/LinearPrograms.h
+++ b/include/PetriEngine/Simplification/LinearPrograms.h
@@ -31,9 +31,11 @@ namespace PetriEngine {
 
                 virtual void clear() = 0;
                 virtual void reset() = 0;
+                //virtual AbstractProgramCollection clone() = 0;
                 virtual size_t size() const = 0;
                 virtual bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) = 0;
 
+
                 virtual uint32_t explorePotency(const PQL::SimplificationContext& context,
                                                 std::vector<uint32_t> &potencies,
                                                 uint32_t maxConfigurationsSolved = std::numeric_limits<uint32_t>::max());
diff --git a/include/PetriEngine/Simplification/Member.h b/include/PetriEngine/Simplification/Member.h
index c30801b5b..a672d39b5 100644
--- a/include/PetriEngine/Simplification/Member.h
+++ b/include/PetriEngine/Simplification/Member.h
@@ -4,6 +4,7 @@
 #include <functional>
 #include <cassert>
 #include <cstring>
+#include <cstdint>
 //#include "../PQL/PQL.h"
 
 namespace PetriEngine {
diff --git a/include/PetriEngine/options.h b/include/PetriEngine/options.h
index 49f29a216..3df53c6f2 100644
--- a/include/PetriEngine/options.h
+++ b/include/PetriEngine/options.h
@@ -62,7 +62,7 @@ struct options_t {
     StatisticsLevel printstatistics = StatisticsLevel::Full;
     std::set<size_t> querynumbers;
     Strategy strategy = Strategy::DEFAULT;
-    int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, initPotencyTimeout = 10;
+    int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, lpPrintLevel = 0, initPotencyTimeout = 10;
     TraceLevel trace = TraceLevel::None;
     bool use_query_reductions = true;
     uint32_t siphontrapTimeout = 0;
diff --git a/include/PetriParse/PNMLParser.h b/include/PetriParse/PNMLParser.h
index 061377ca1..3b841c892 100644
--- a/include/PetriParse/PNMLParser.h
+++ b/include/PetriParse/PNMLParser.h
@@ -79,6 +79,10 @@ class PNMLParser {
         return queries;
     }
 
+    void parseMarking(
+        const rapidxml::xml_document<>& doc,
+        PetriEngine::AbstractPetriNetBuilder* builder,
+        ColorTypeMap* colorTypes);
 private:
     void parseElement(rapidxml::xml_node<>* element);
     void parsePlace(rapidxml::xml_node<>* element);
diff --git a/include/utils/structures/shared_string.h b/include/utils/structures/shared_string.h
index 3cc41398c..f2de0f2da 100644
--- a/include/utils/structures/shared_string.h
+++ b/include/utils/structures/shared_string.h
@@ -14,6 +14,7 @@
 #include <string>
 #include <memory>
 #include <algorithm>
+#include <cstdint>
 
 typedef const std::string const_string;
 typedef std::shared_ptr<const_string> shared_const_string;
diff --git a/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp b/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp
index 0e00c2bea..594d6fee6 100644
--- a/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp
+++ b/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp
@@ -35,9 +35,12 @@ namespace PetriEngine {
 
     ColoredPetriNetBuilder::~ColoredPetriNetBuilder() {
         // cleaning up colors
-        for(auto& e : _colors)
-            if(e.second != Colored::ColorType::dotInstance())
-                delete e.second;
+        if (_ownsColors)
+        {
+            for(auto& e : _colors)
+                if(e.second != Colored::ColorType::dotInstance())
+                    delete e.second;
+        }
         for(auto& v : _variables)
             delete v;
         _colors.clear();
diff --git a/src/PetriEngine/Colored/PnmlWriter.cpp b/src/PetriEngine/Colored/PnmlWriter.cpp
index c481179fd..d14fb9b09 100644
--- a/src/PetriEngine/Colored/PnmlWriter.cpp
+++ b/src/PetriEngine/Colored/PnmlWriter.cpp
@@ -16,6 +16,21 @@ namespace PetriEngine {
             metaInfoClose();
         }
 
+        void PnmlWriter::writeInitialTokens(const std::string& placeId)
+        {
+            const auto it = std::find_if(
+                _builder._placenames.begin(),
+                _builder._placenames.end(),
+                [&](const auto& kv) {return placeId == *kv.first;});
+
+            if (it == _builder._placenames.end())
+            {
+                throw base_error("Could not write initial tokens, since the place '", placeId, "' does not exist");
+            }
+
+            handleTokenExpression(_builder.places()[it->second].marking);
+        }
+
         void PnmlWriter::metaInfo() {
             _out << getTabs() << "<?xml version=\"1.0\"?>\n"
                  << getTabs() << "<pnml xmlns=\"http://www.pnml.org/version-2009/grammar/pnml\">\n"
@@ -60,10 +75,8 @@ namespace PetriEngine {
 
                 //this is a hack, better way to find if a color is a finite int range?
                 if (is_number(types[0]->operator[](size_t{0}).getColorName())) {
-                    _namedSortTypes.emplace(colortype->getName(), "finite range");
                     handleFiniteRange(types);
                 } else {
-                    _namedSortTypes.emplace(colortype->getName(), "cyclic enumeration");
                     if (types[0]->getName() == "dot") {
                         _out << increaseTabs() << "<dot/>\n";
                     } else {
@@ -216,11 +229,19 @@ namespace PetriEngine {
             _out << increaseTabs() << "<text>" << marking.toString() << "</text>\n";
             _out << getTabs() << "<structure>\n";
 
-            if (marking.size() > 1) {
+            handleTokenExpression(marking);
+
+            _out << decreaseTabs() << "</structure>\n";
+            _out << decreaseTabs() << "</hlinitialMarking>\n";
+        }
+
+        void PnmlWriter::handleTokenExpression(const Multiset& tokens)
+        {
+            if (tokens.size() > 1) {
                 bool first = true;
                 _out << increaseTabs() << "<add>\n";
 
-                for (const auto &p: marking) {
+                for (const auto &p: tokens) {
                     if (p.second == 0) {
                         continue;
                     }
@@ -235,16 +256,13 @@ namespace PetriEngine {
                 }
                 _out << decreaseTabs() << "</add>\n";
             } else {
-                for (const auto &p: marking) {
+                for (const auto &p: tokens) {
                     if (p.second == 0) {
                         continue;
                     }
                     handleNumberOf(p);
                 }
             }
-
-            _out << decreaseTabs() << "</structure>\n";
-            _out << decreaseTabs() << "</hlinitialMarking>\n";
         }
 
         void PnmlWriter::handleNumberOf(std::pair<const PetriEngine::Colored::Color *const, uint32_t> numberOff) {
diff --git a/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp b/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
index c35ec229d..72746a037 100644
--- a/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
+++ b/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
@@ -1,12 +1,13 @@
 #include "PetriEngine/ExplicitColored/ColoredResultPrinter.h"
-
 #include <iomanip>
+#include "PetriEngine/Colored/PnmlWriter.h"
+
 
 namespace PetriEngine::ExplicitColored {
     void ColoredResultPrinter::printResult(
         const SearchStatistics& searchStatistics,
         const Reachability::AbstractHandler::Result result,
-        const std::vector<TraceStep>* trace
+        const ExplicitColoredTraceContext* trace
     ) const {
         _printCommon(result, {});
         _stream << "STATS:" << std::endl
@@ -59,10 +60,10 @@ namespace PetriEngine::ExplicitColored {
         std::cout << "satisfied" << std::endl;
     }
 
-    void ColoredResultPrinter::_printTrace(const std::vector<TraceStep>& trace) const {
+    void ColoredResultPrinter::_printTrace(const ExplicitColoredTraceContext& trace) const {
         _traceStream << "Trace: " << std::endl;
         _traceStream << "<trace>" << std::endl;
-        for (const auto& step : trace) {
+        for (const auto& step : trace.traceSteps) {
             if (!step.isInitial) {
                 _traceStream << "\t<transition id=" << std::quoted(step.transitionId) << ">" << std::endl;
                 _traceStream << "\t\t<bindings>" << std::endl;
@@ -75,24 +76,70 @@ namespace PetriEngine::ExplicitColored {
                 _traceStream << "\t</transition>" << std::endl;
             }
             _traceStream << "\t<marking>" << std::endl;
-            for (const auto& [placeId, marking] : step.marking) {
-                if (!marking.empty()) {
-                    _traceStream << "\t\t<place id=" << std::quoted(placeId) << ">" << std::endl;
-                    for (const auto& [productColor, count] : marking) {
-                        if (count > 0) {
-                            _traceStream << "\t\t\t<token count=" << std::quoted(std::to_string(count)) << ">" << std::endl;
-                            for (const auto& color : productColor) {
-                                _traceStream << "\t\t\t\t<color>" << color << "</color>" << std::endl;
-                            }
-                            _traceStream << "\t\t\t</token>" << std::endl;
-                        }
+            _printMarkings(trace.cpnBuilder, step);
+            _traceStream << "\t</marking>" << std::endl;
+        }
+        _traceStream << "</trace>" << std::endl;
+    }
+
+    void ColoredResultPrinter::_printMarkings(
+        const ExplicitColoredPetriNetBuilder& explicitCpnBuilder, const TraceStep& traceStep) const
+    {
+        shared_string_set sharedStringSet {};
+        ColoredPetriNetBuilder builder(sharedStringSet);
+        for (const auto colorType : explicitCpnBuilder.getUnderlyingVariableColorTypes())
+        {
+            builder.addColorType(colorType->getName(), colorType);
+        }
+
+        for (const auto& [place_id, traceTokens] : traceStep.marking) {
+            const auto place = explicitCpnBuilder.getPlaceIndices().find(place_id)->second;
+
+            Colored::Multiset tokens;
+            const auto& colorType = *explicitCpnBuilder.getPlaceUnderlyingColorType(place);
+            for (const auto& [color, count] : traceTokens)
+            {
+                if (color.size() > 1)
+                {
+                    const auto productColorType = dynamic_cast<const Colored::ProductType*>(&colorType);
+                    if (productColorType == nullptr) {
+                        throw std::runtime_error("Trace color is inconsistent with underlying color type");
                     }
-                    _traceStream << "\t\t</place>" << std::endl;
+
+                    std::vector<uint32_t> colorIndices;
+                    for (size_t colorTypeIndex = 0; colorTypeIndex < color.size(); colorTypeIndex++) {
+                        colorIndices.push_back(
+                            (*productColorType->getNestedColorType(colorTypeIndex))[color[colorTypeIndex]]->getId());
+                    }
+
+                    tokens[productColorType->getColor(colorIndices)] = count;
+                }
+                else
+                {
+                    tokens[colorType[color[0]]] = count;
                 }
             }
-            _traceStream << "\t</marking>" << std::endl;
+
+            builder.addPlace(
+                explicitCpnBuilder.getPlaceName(place),
+                explicitCpnBuilder.getPlaceUnderlyingColorType(place),
+                std::move(tokens),
+                0,
+                0);
+        }
+
+        Colored::PnmlWriter writer(builder, _traceStream);
+        builder.leak_colors();
+
+        for (const auto& [place_id, traceTokens] : traceStep.marking)
+        {
+            if (!traceTokens.empty())
+            {
+                _traceStream << "\t\t<place id=" << std::quoted(place_id) << ">" << std::endl;
+                writer.writeInitialTokens(place_id);
+                _traceStream << "\t\t</place>" << std::endl;
+            }
         }
-        _traceStream << "</trace>" << std::endl;
     }
 }
 
diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp
index 075035a1d..f5e11b1dc 100644
--- a/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp
+++ b/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp
@@ -8,6 +8,10 @@
 #include <iomanip>
 #include <PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h>
 #include <PetriEngine/ExplicitColored/SuccessorGenerator/ColoredSuccessorGenerator.h>
+#include <PetriEngine/Colored/ColoredPetriNetBuilder.h>
+#include <PetriEngine/Colored/PnmlWriter.h>
+
+#include "PetriParse/PNMLParser.h"
 
 namespace PetriEngine::ExplicitColored {
     int ExplicitColoredInteractiveMode::run(const std::string &model_path) {
@@ -33,7 +37,7 @@ namespace PetriEngine::ExplicitColored {
     ExplicitColoredInteractiveMode::ExplicitColoredInteractiveMode(
         const ColoredSuccessorGenerator& successorGenerator,
         const ColoredPetriNet& cpn,
-        const ExplicitColoredPetriNetBuilder& builder
+        ExplicitColoredPetriNetBuilder& builder
     )
     : _successorGenerator(successorGenerator), _cpn(cpn), _builder(builder) { }
 
@@ -115,6 +119,9 @@ namespace PetriEngine::ExplicitColored {
     }
 
     void ExplicitColoredInteractiveMode::_printValidBindings(std::ostream &out, const ColoredPetriNetMarking &currentMarking) const {
+        // We always use the same state id in interactive mode, therefore we need to shrink state everytime
+        // to clear the generated color constraint data
+        _successorGenerator.shrinkState(0);
         out << "<valid-bindings>" << std::endl;
         for (Transition_t transition = 0; transition < _cpn.getTransitionCount(); transition++) {
             Binding_t currentBinding = 0;
@@ -163,92 +170,8 @@ namespace PetriEngine::ExplicitColored {
     std::optional<ColoredPetriNetMarking> ExplicitColoredInteractiveMode::_parseMarking(
         const rapidxml::xml_document<>& markingXml,
         std::ostream& errorOut
-    ) const {
-        const auto root = markingXml.first_node();
-
-        ColoredPetriNetMarking generatedMarking;
-        generatedMarking.markings.resize(_builder.getPlaceCount());
-
-        auto placeNode = root->first_node();
-        if (root->name() != std::string("marking")) {
-            errorOut << "Unexpected tag " << std::quoted(root->name()) << std::endl;
-            return std::nullopt;
-        }
-
-        if (placeNode == nullptr) {
-            return generatedMarking; // Empty marking
-        }
-
-        do {
-            if (placeNode->name() != std::string("place")) {
-                errorOut << "Unexpected tag " << std::quoted(placeNode->name()) << std::endl;
-                return std::nullopt;
-            }
-
-            if (placeNode->first_attribute("id") == nullptr) {
-                errorOut << "Place tag is missing id attribute" << std::endl;
-                return std::nullopt;
-            }
-
-            auto markingPlaceIndexIt = _builder.getPlaceIndices().find(placeNode->first_attribute("id")->value());
-            if (markingPlaceIndexIt == _builder.getPlaceIndices().end()) {
-                errorOut << "Unknown place id " << std::quoted(placeNode->first_attribute("id")->value()) << std::endl;
-                return std::nullopt;
-            }
-            auto tokenNode = placeNode->first_node();
-            auto placeColorType = _builder.getPlaceUnderlyingColorType(markingPlaceIndexIt->second);
-            do {
-                if (tokenNode->name() != std::string("token")) {
-                    errorOut << "Unexpected tag " << std::quoted(tokenNode->name()) << std::endl;
-                    return std::nullopt;
-                }
-                if (tokenNode->first_attribute("count") == nullptr) {
-                    errorOut << "Token tag is missing count attribute" << std::endl;
-                    return std::nullopt;
-                }
-                auto count = 0;
-                try {
-                    count = std::stoi(tokenNode->first_attribute("count")->value());
-                } catch (const std::out_of_range&) {
-                    errorOut << "Token count " << tokenNode->first_attribute("count")->value() << " is too big or too small" << std::endl;
-                    return std::nullopt;
-                } catch (const std::invalid_argument&) {
-                    errorOut << "Token count " << tokenNode->first_attribute("count")->value() << " could not be parsed" << std::endl;
-                    return std::nullopt;
-                }
-                auto colorComponentNode = tokenNode->first_node();
-                uint64_t encodedColor = 0;
-                const auto& colorCodec = _cpn.getPlaces()[markingPlaceIndexIt->second].colorType->colorCodec;
-                auto componentIndex = 0;
-                do {
-                    if (colorComponentNode->name() != std::string("color")) {
-                        errorOut << "Unexpected tag " << colorComponentNode->name() << std::endl;
-                        return std::nullopt;
-                    }
-                    if (colorComponentNode->type() != rapidxml::node_element) {
-                        errorOut << "Expected color tag to only contain color id" << std::endl;
-                        return std::nullopt;
-                    }
-                    const auto colorName = colorComponentNode->value();
-                    auto currentColorType = placeColorType;
-                    if (auto productColor = dynamic_cast<const Colored::ProductType*>(placeColorType)) {
-                        currentColorType = productColor->getNestedColorType(componentIndex);
-                    }
-
-                    auto colorIndex = _findColorIndex(currentColorType, colorName);
-                    if (colorIndex == std::nullopt) {
-                        errorOut << "Unknown color id " << std::quoted(colorName) << std::endl;
-                        return std::nullopt;
-                    }
-                    encodedColor = colorCodec.addToValue(encodedColor, componentIndex, *colorIndex);
-
-                    componentIndex++;
-                } while ((colorComponentNode = colorComponentNode->next_sibling()) != nullptr);
-                generatedMarking.markings[markingPlaceIndexIt->second].addCount(encodedColor, count);
-            } while ((tokenNode = tokenNode->next_sibling()) != nullptr);
-        } while ((placeNode = placeNode->next_sibling()) != nullptr);
-
-        return generatedMarking;
+    ) {
+        return _builder.parseMarking(markingXml);
     }
 
     std::optional<std::pair<Transition_t, Binding>> ExplicitColoredInteractiveMode::_parseTransition(
@@ -333,37 +256,55 @@ namespace PetriEngine::ExplicitColored {
         std::ostream &out,
         const ColoredPetriNetMarking &currentMarking
     ) const {
-        out << "<marking>" << std::endl;
-        for (Place_t place = 0; place < currentMarking.markings.size(); place++) {
-            out << "\t<place id=" << std::quoted(_builder.getPlaceName(place)) << ">" << std::endl;
+        shared_string_set sharedStringSet {};
+        ColoredPetriNetBuilder builder(sharedStringSet);
+        builder.leak_colors();
+        for (Place_t place = 0; place < currentMarking.markings.size(); place++)
+        {
+            builder.addColorType(_builder.getPlaceName(place), _builder.getPlaceUnderlyingColorType(place));
+
+            Colored::Multiset tokens;
             const auto& colorCodec = _cpn.getPlaces()[place].colorType->colorCodec;
             const auto& colorType = *_builder.getPlaceUnderlyingColorType(place);
             for (const auto& [encodedColor, count] : currentMarking.markings[place].counts()) {
                 if (count > 0) {
-                    out << "\t\t<token count=" << std::quoted(std::to_string(count)) << ">" << std::endl;
                     if (colorCodec.getColorCount() > 1) {
                         const auto productColorType = dynamic_cast<const Colored::ProductType*>(&colorType);
                         if (productColorType == nullptr) {
                             throw std::runtime_error("Color codec is inconsistent with underlying color type");
                         }
+                        std::vector<uint32_t> colorIndices;
                         for (size_t colorIndex = 0; colorIndex < colorCodec.getColorCount(); colorIndex++) {
-                            const Color_t color = colorCodec.decode(encodedColor, colorIndex);
-                            out << "\t\t\t<color>"
-                                << (*(productColorType->getNestedColorType(colorIndex)))[color].getColorName()
-                                << "</color>"
-                                << std::endl;
+                            colorIndices.push_back(colorCodec.decode(encodedColor, colorIndex));
                         }
+
+                        tokens[productColorType->getColor(colorIndices)] += count;
                     } else {
-                        out << "\t\t\t<color>"
-                            << colorType[encodedColor].getColorName()
-                            << "</color>"
-                            << std::endl;
+                        tokens[&colorType[encodedColor]] += count;
                     }
-                    out << "\t\t</token>" << std::endl;
                 }
             }
-            out << "\t</place>" << std::endl;
+
+            builder.addPlace(
+                _builder.getPlaceName(place),
+                _builder.getPlaceUnderlyingColorType(place),
+                std::move(tokens),
+                0,
+                0);
+        }
+
+
+        Colored::PnmlWriter pnmlWriter(builder, out);
+        out << "<marking>" << std::endl;
+        for (Place_t place = 0; place < currentMarking.markings.size(); place++) {
+            if (currentMarking.markings[place].totalCount() > 0)
+            {
+                out << "\t<place id=" << std::quoted(_builder.getPlaceName(place)) << ">" << std::endl;
+                pnmlWriter.writeInitialTokens(_builder.getPlaceName(place));
+                out << "\t</place>" << std::endl;
+            }
         }
         out << "</marking>" << std::endl;
+
     }
 }
diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp
index 2f5882ab7..3cc4d9b96 100644
--- a/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp
+++ b/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp
@@ -238,7 +238,7 @@ namespace PetriEngine::ExplicitColored {
         return Result::UNKNOWN;
     }
 
-    std::pair<ExplicitColoredModelChecker::Result, std::optional<std::vector<TraceStep>>> ExplicitColoredModelChecker::explicitColorCheck(
+    std::pair<ExplicitColoredModelChecker::Result, std::optional<ExplicitColoredTraceContext>> ExplicitColoredModelChecker::explicitColorCheck(
         const std::string& pnmlModel,
         const Condition_ptr& query,
         options_t& options,
@@ -268,18 +268,18 @@ namespace PetriEngine::ExplicitColored {
             *searchStatistics = worklist.GetSearchStatistics();
         }
 
-        std::optional<std::vector<TraceStep>> trace = std::nullopt;
+        std::optional<ExplicitColoredTraceContext> traceContext = std::nullopt;
         if (options.trace != TraceLevel::None) {
             auto counterExample = worklist.getCounterExampleId();
 
             if (counterExample.has_value()) {
                 auto internalTrace  = worklist.getTraceTo(counterExample.value());
                 if (internalTrace.has_value()) {
-                    trace = _translateTraceStep(internalTrace.value(), cpnBuilder, net);
+                    traceContext.emplace(_translateTraceStep(internalTrace.value(), cpnBuilder, net), std::move(cpnBuilder));
                 }
             }
         }
-        return std::make_pair(result ? Result::SATISFIED : Result::UNSATISFIED, trace);
+        return std::make_pair(result ? Result::SATISFIED : Result::UNSATISFIED, std::move(traceContext));
     }
 
     void ExplicitColoredModelChecker::_reduce(
diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp
index 6defb57cb..09ed11eba 100644
--- a/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp
+++ b/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp
@@ -2,6 +2,7 @@
 #include "PetriEngine/ExplicitColored/ExpressionCompilers/ArcCompiler.h"
 #include "PetriEngine/ExplicitColored/ExpressionCompilers/GuardCompiler.h"
 #include <algorithm>
+#include "PetriParse/PNMLParser.h"
 
 namespace PetriEngine::ExplicitColored {
     ExplicitColoredPetriNetBuilder::ExplicitColoredPetriNetBuilder() {
@@ -156,6 +157,34 @@ namespace PetriEngine::ExplicitColored {
         colorType->addType(newConstituent);
     }
 
+    void ExplicitColoredPetriNetBuilder::addTokens(std::string&& place, Colored::Multiset&& tokens)
+    {
+        const auto placeId = _placeIndices.find(place);
+        if (placeId == _placeIndices.end())
+        {
+            throw base_error("Unknown place name ", place);
+        }
+
+        const auto underlyingColorType = getPlaceUnderlyingColorType(placeId->second);
+
+        CPNMultiSet multiSet;
+        const auto& colorType = _colorTypeMap.find(underlyingColorType->getName())->second;
+        for (const auto& [tokenColor, count] : tokens) {
+            std::vector<Color_t> colorSequence;
+            if (tokenColor->isTuple()) {
+                for (const auto& color : tokenColor->getTupleColors()) {
+                    colorSequence.push_back(color->getId());
+                }
+            } else {
+                colorSequence.push_back(tokenColor->getId());
+            }
+            multiSet.setCount(ColorSequence{colorSequence, *colorType}, count);
+        }
+
+
+        _standAloneMarking.markings[placeId->second] = multiSet;
+    }
+
     void ExplicitColoredPetriNetBuilder::addVariable(const Colored::Variable* variable) {
         (*_variableMap)[variable->name] = _variableMap->size();
         const auto colorType = _colorTypeMap.find(variable->colorType->getName())->second;
@@ -203,6 +232,15 @@ namespace PetriEngine::ExplicitColored {
         return std::move(_currentNet);
     }
 
+    ColoredPetriNetMarking ExplicitColoredPetriNetBuilder::parseMarking(const rapidxml::xml_document<>& doc)
+    {
+        _standAloneMarking = ColoredPetriNetMarking();
+        _standAloneMarking.markings.resize(getPlaceCount());
+        PNMLParser parser;
+        parser.parseMarking(doc, this, _colors.get());
+        return _standAloneMarking;
+    }
+
     void ExplicitColoredPetriNetBuilder::_createArcsAndTransitions() {
         const auto transitions = _currentNet._transitions.size();
         auto transIndices = std::vector<std::pair<uint32_t,uint32_t>>(transitions + 1);
diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp
index f0fb0b404..6090c8047 100644
--- a/src/PetriEngine/PQL/Contexts.cpp
+++ b/src/PetriEngine/PQL/Contexts.cpp
@@ -68,6 +68,11 @@ namespace PetriEngine {
             return _potencyTimeout;
         }
 
+        uint32_t SimplificationContext::getPrintLevel() const 
+        {
+            return _lpPrintLevel;
+        }
+
         double SimplificationContext::getReductionTime()
         {
             // duration in seconds
diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp
index 85499d9b6..218161f9d 100644
--- a/src/PetriEngine/PQL/Simplifier.cpp
+++ b/src/PetriEngine/PQL/Simplifier.cpp
@@ -30,6 +30,7 @@ namespace PetriEngine { namespace PQL {
     }
 
     AbstractProgramCollection_ptr mergeLps(std::vector<AbstractProgramCollection_ptr> &&lps) {
+        //std::cout << "merging Lps with " << lps.size() << " Elements\n";
         if (lps.size() == 0) return nullptr;
         int j = 0;
         int i = lps.size() - 1;
@@ -44,12 +45,60 @@ namespace PetriEngine { namespace PQL {
         return lps[0];
     }
 
-    Retval Simplifier::simplify_or(const LogicalCondition *element) {
 
+     AbstractProgramCollection_ptr createGlobalUnion(AbstractProgramCollection_ptr &global_lp, std::vector<AbstractProgramCollection_ptr> &&nonglobal_lps) {
+        //std::cout << "creating unioncollection of global and nonglobal conditions\n";
+        
+        if(global_lp == nullptr){
+            //std::cout << "global_lp is NULL\n";
+            if(nonglobal_lps.size() == 0){
+                //std::cout << "returning null from createGlobalUnion\n";
+                return nullptr;
+            }else{
+                return std::make_shared<UnionCollection>(std::move(nonglobal_lps));
+            }
+        }
+
+        if(nonglobal_lps.size() == 0){
+            //std::cout << "nonglobal_lps is empty\n";
+            return global_lp;
+        }
+        
+
+        std::vector<AbstractProgramCollection_ptr> merges;
+
+        for(int i = 0; i < nonglobal_lps.size(); i++){
+            merges.emplace_back(std::make_shared<MergeCollection>(global_lp, nonglobal_lps[i]));
+        }
+
+        return std::make_shared<UnionCollection>(std::move(merges));
+     }
+
+    Retval Simplifier::simplify_or(const LogicalCondition *element) {
+        //std::cout << "simplifying or\n";
         std::vector<Condition_ptr> conditions;
-        std::vector<AbstractProgramCollection_ptr> lps, neglpsv;
+        std::vector<AbstractProgramCollection_ptr> lps;
+        std::vector<AbstractProgramCollection_ptr> unquantified_neglpsv;
+        std::vector<AbstractProgramCollection_ptr> global_neglpsv;
+        std::vector<AbstractProgramCollection_ptr> nonglobal_neglpsv;
+        
+        const bool same_context = qparent_neg_context == _context.negated();
+        const bool parent_final = quantifier_parent == LPQUANT::FINAL;
+        const bool parent_global = quantifier_parent == LPQUANT::GLOBAL;
+        const bool neg_is_invariant = (same_context && parent_final) || (!same_context && parent_global);
+
+        const auto local_parent = quantifier_parent;
+
         for (const auto &c: element->getOperands()) {
+            quantifier_found = LPQUANT::NONE;
+            int32_t pre_quantifiers = quantifiers;
+            if(!neg_is_invariant)
+                quantifier_parent = LPQUANT::OTHER;
             Visitor::visit(this, c);
+            quantifier_parent = local_parent;
+
+            //std::cout << "sub expression quant depth: " << quantifiers - pre_quantifiers << "\n";
+            
             auto r = std::move(_return_value);
             assert(r.neglps);
             assert(r.lps);
@@ -59,17 +108,54 @@ namespace PetriEngine { namespace PQL {
             } else if (r.formula->isTriviallyFalse()) {
                 continue;
             }
+
             conditions.push_back(r.formula);
-            lps.push_back(r.lps);
-            neglpsv.emplace_back(r.neglps);
+
+
+            lps.emplace_back(r.lps);
+
+            if( ( quantifiers - pre_quantifiers ) > 1){
+                nonglobal_neglpsv.emplace_back(r.neglps);
+            }else if(quantifier_found == LPQUANT::NONE){
+                if(neg_is_invariant){
+                    global_neglpsv.emplace_back(r.neglps);
+                }else{
+                    unquantified_neglpsv.emplace_back(r.neglps);
+                }
+            }else if(quantifier_found == LPQUANT::FINAL){
+                global_neglpsv.emplace_back(r.neglps);
+            }else{
+                nonglobal_neglpsv.emplace_back(r.neglps);
+            }
         }
 
-        AbstractProgramCollection_ptr neglps = mergeLps(std::move(neglpsv));
+        //std::cout << "sizes  or: " << lps.size() << ", " << global_neglpsv.size() << ", " << nonglobal_neglpsv.size() << "\n";
 
         if (conditions.size() == 0) {
             return Retval(BooleanCondition::FALSE_CONSTANT);
         }
 
+        if(unquantified_neglpsv.size() > 0){
+            auto uq_neglps = mergeLps(std::move(unquantified_neglpsv));
+            nonglobal_neglpsv.emplace_back(uq_neglps);
+        }
+
+        if(global_neglpsv.size() > 0 && nonglobal_neglpsv.size() > 0){
+            auto id = std::chrono::duration_cast<std::chrono::microseconds>(_context._id.time_since_epoch()).count();
+            std::cout << "# MERGE RULE APPLIED " << id << "\n";
+        }
+
+        AbstractProgramCollection_ptr neglps = mergeLps(std::move(global_neglpsv));
+        neglps = createGlobalUnion(neglps, std::move(nonglobal_neglpsv));
+
+        if(neglps == nullptr){
+            neglps = std::make_shared<SingleProgram>();
+        }
+
+        if(lps.size() == 0){
+            lps.emplace_back(std::make_shared<SingleProgram>());
+        }
+        
         try {
             if (!_context.timeout() && !neglps->satisfiable(_context)) {
                 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -83,7 +169,7 @@ namespace PetriEngine { namespace PQL {
         // Lets try to see if the r1 AND r2 can ever be false at the same time
         // If not, then we know that r1 || r2 must be true.
         // we check this by checking if !r1 && !r2 is unsat
-
+        //std::cout << "leaving or\n";
         return Retval(
                 makeOr(conditions),
                 std::make_shared<UnionCollection>(std::move(lps)),
@@ -91,12 +177,30 @@ namespace PetriEngine { namespace PQL {
     }
 
     Retval Simplifier::simplify_and(const LogicalCondition *element) {
-
+        //std::cout << "simplifying and\n";
         std::vector<Condition_ptr> conditions;
-        std::vector<AbstractProgramCollection_ptr> lpsv;
+        std::vector<AbstractProgramCollection_ptr> global_lpsv;
+        std::vector<AbstractProgramCollection_ptr> unquantified_lpsv;
+        std::vector<AbstractProgramCollection_ptr> nonglobal_lpsv;
         std::vector<AbstractProgramCollection_ptr> neglps;
+
+        const bool same_context = qparent_neg_context == _context.negated();
+        const bool parent_final = quantifier_parent == LPQUANT::FINAL;
+        const bool parent_global = quantifier_parent == LPQUANT::GLOBAL;
+        const bool is_invariant = (same_context && parent_global) || (!same_context && parent_final);
+
+        const auto local_parent = quantifier_parent;
+
         for (auto &c: element->getOperands()) {
+            quantifier_found = LPQUANT::NONE;
+            int32_t pre_quantifiers = quantifiers;
+            if(!is_invariant)
+                quantifier_parent = LPQUANT::OTHER;
             Visitor::visit(this, c);
+            quantifier_parent = local_parent;
+
+            //std::cout << "sub expression quant depth: " << quantifiers - pre_quantifiers << "\n";
+            
             auto r = std::move(_return_value);
             if (r.formula->isTriviallyFalse()) {
                 return Retval(BooleanCondition::FALSE_CONSTANT);
@@ -105,15 +209,49 @@ namespace PetriEngine { namespace PQL {
             }
 
             conditions.push_back(r.formula);
-            lpsv.emplace_back(r.lps);
+
+            if( ( quantifiers - pre_quantifiers ) > 1){
+                nonglobal_lpsv.emplace_back(r.lps);
+            }else if(quantifier_found == LPQUANT::NONE){
+                if(is_invariant){
+                    global_lpsv.emplace_back(r.lps);
+                }else{
+                    unquantified_lpsv.emplace_back(r.lps);
+                }
+            }else if (quantifier_found == LPQUANT::GLOBAL){
+                global_lpsv.emplace_back(r.lps);
+            }else{
+                nonglobal_lpsv.emplace_back(r.lps);
+            }
             neglps.emplace_back(r.neglps);
         }
 
+        //std::cout << "sizes and: " << neglps.size() << ", " << global_lpsv.size() << ", " << nonglobal_lpsv.size() << "\n";
+
+        
         if (conditions.size() == 0) {
             return Retval(BooleanCondition::TRUE_CONSTANT);
         }
 
-        auto lps = mergeLps(std::move(lpsv));
+         if(unquantified_lpsv.size() > 0){
+            auto uq_lps = mergeLps(std::move(unquantified_lpsv));
+            nonglobal_lpsv.emplace_back(uq_lps);
+        }
+
+        if(global_lpsv.size() > 0 && nonglobal_lpsv.size() > 0){
+            auto id = std::chrono::duration_cast<std::chrono::microseconds>(_context._id.time_since_epoch()).count();
+            std::cout << "# MERGE RULE APPLIED " << id << "\n";
+        }
+        auto lps = mergeLps(std::move(global_lpsv));
+        lps = createGlobalUnion(lps, std::move(nonglobal_lpsv));
+        
+        if(lps == nullptr){
+            lps = std::make_shared<SingleProgram>();
+        }
+
+        if(neglps.size() == 0){
+            neglps.emplace_back(std::make_shared<SingleProgram>());
+        }
 
         try {
             if (!_context.timeout() && !lps->satisfiable(_context)) {
@@ -125,10 +263,12 @@ namespace PetriEngine { namespace PQL {
             std::cout << "Query reduction: memory exceeded during LPS merge." << std::endl;
         }
 
+        
         // Lets try to see if the r1 AND r2 can ever be false at the same time
         // If not, then we know that r1 || r2 must be true.
         // we check this by checking if !r1 && !r2 is unsat
 
+
         return Retval(
                 makeAnd(conditions),
                 std::move(lps),
@@ -198,15 +338,56 @@ namespace PetriEngine { namespace PQL {
         }
     }
 
+    /*Retval Simplifier::simplify_global_quantifier(Retval &r) {
+        //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n";
+        //std::cout << "triv false: " << r.formula->isTriviallyFalse() << "\n";
+        quantifier_found = LPQUANT::GLOBAL;
+        if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) {
+            return Retval(BooleanCondition::TRUE_CONSTANT);
+        } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) {
+            return Retval(BooleanCondition::FALSE_CONSTANT);
+        } else {
+            return Retval(std::make_shared<GCondition>(r.formula), r.lps, r.neglps);
+        }
+    }*/
+
     template<typename Quantifier>
     Retval Simplifier::simplify_simple_quantifier(Retval &r) {
+        //std::cout << "other quantifier\n";
         static_assert(std::is_base_of_v<SimpleQuantifierCondition, Quantifier>);
+        quantifier_found = LPQUANT::OTHER;
+        //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n";
+        //std::cout << "triv false: " << r.formula->isTriviallyFalse() << "\n";
         if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) {
             return Retval(BooleanCondition::TRUE_CONSTANT);
         } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) {
             return Retval(BooleanCondition::FALSE_CONSTANT);
         } else {
-            return Retval(std::make_shared<Quantifier>(r.formula));
+            return Retval(std::make_shared<Quantifier>(r.formula), r.lps, r.neglps);
+        }
+    }
+
+    template<>
+    Retval Simplifier::simplify_simple_quantifier<GCondition>(Retval &r){
+        quantifier_found = LPQUANT::GLOBAL;
+        if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) {
+            return Retval(BooleanCondition::TRUE_CONSTANT);
+        } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) {
+            return Retval(BooleanCondition::FALSE_CONSTANT);
+        } else {
+            return Retval(std::make_shared<GCondition>(r.formula), r.lps, r.neglps);
+        }
+    }
+
+    template<>
+    Retval Simplifier::simplify_simple_quantifier<FCondition>(Retval &r){
+        quantifier_found = LPQUANT::FINAL;
+        if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) {
+            return Retval(BooleanCondition::TRUE_CONSTANT);
+        } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) {
+            return Retval(BooleanCondition::FALSE_CONSTANT);
+        } else {
+            return Retval(std::make_shared<FCondition>(r.formula), r.lps, r.neglps);
         }
     }
 
@@ -300,6 +481,7 @@ namespace PetriEngine { namespace PQL {
     /******* Simplifier accepts ********/
 
     void Simplifier::_accept(const NotCondition *element) {
+        //std::cout << "negating\n";
         _context.negate();
         Visitor::visit(this, element->getCond());
         _context.negate();
@@ -831,6 +1013,8 @@ namespace PetriEngine { namespace PQL {
     void Simplifier::_accept(const UntilCondition *condition) {
         bool neg = _context.negated();
         _context.setNegate(false);
+        quantifiers++;
+        quantifier_parent = LPQUANT::OTHER;
 
         Visitor::visit(this, condition->getCond2());
         Retval r2 = std::move(_return_value);
@@ -845,6 +1029,7 @@ namespace PetriEngine { namespace PQL {
                            Retval(BooleanCondition::TRUE_CONSTANT) :
                            Retval(BooleanCondition::FALSE_CONSTANT))
         }
+        quantifier_parent = LPQUANT::OTHER;
         Visitor::visit(this, condition->getCond1());
         Retval r1 = std::move(_return_value);
 
@@ -895,18 +1080,47 @@ namespace PetriEngine { namespace PQL {
     }
 
     void Simplifier::_accept(const FCondition *condition) {
+        quantifiers++;
+        if(_context.negated()){
+            quantifier_parent = LPQUANT::GLOBAL;
+        }else{
+            quantifier_parent = LPQUANT::FINAL;
+        }
+        qparent_neg_context = _context.negated();
         Visitor::visit(this, condition->getCond());
-        RETURN(_context.negated() ? simplify_simple_quantifier<GCondition>(_return_value)
-                                         : simplify_simple_quantifier<FCondition>(_return_value))
+        if(_context.negated()){
+            //std::cout << "negated GCondition\n";
+            auto r = simplify_simple_quantifier<GCondition>(_return_value);
+            RETURN(std::move(r));
+        }else{
+            //std::cout << "FCondition\n";
+            RETURN(simplify_simple_quantifier<FCondition>(_return_value));
+        }
     }
 
     void Simplifier::_accept(const GCondition *condition) {
+        quantifiers++;
+        if(_context.negated()){
+            quantifier_parent = LPQUANT::FINAL;
+        }else{
+            quantifier_parent = LPQUANT::GLOBAL;
+        }
+        qparent_neg_context = _context.negated();
         Visitor::visit(this, condition->getCond());
-        RETURN(_context.negated() ? simplify_simple_quantifier<FCondition>(_return_value)
-                                         : simplify_simple_quantifier<GCondition>(_return_value))
+
+        if(_context.negated()){
+            //std::cout << "negated FCondition\n";
+            RETURN(simplify_simple_quantifier<FCondition>(_return_value));
+        }else{
+            //std::cout << "GCondition\n";
+            auto r  = simplify_simple_quantifier<GCondition>(_return_value);
+            RETURN(std::move(r))
+        }
     }
 
     void Simplifier::_accept(const XCondition *condition) {
+        quantifiers++;
+        quantifier_parent = LPQUANT::OTHER;
         Visitor::visit(this, condition->getCond());
         RETURN(simplify_simple_quantifier<XCondition>(_return_value))
     }
diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp
index 5733e549d..9f822df6f 100644
--- a/src/PetriEngine/Simplification/LinearProgram.cpp
+++ b/src/PetriEngine/Simplification/LinearProgram.cpp
@@ -46,6 +46,70 @@ namespace PetriEngine {
 
         constexpr auto infty = std::numeric_limits<REAL>::infinity();
 
+        std::string bound_or_inf(double bound){
+            std::string inf = "inf";
+            std::string ninf = "ninf";
+            return (std::fabs(bound) != infty)? std::to_string(bound) : ((bound > 0)? inf : ninf);
+        }
+
+        void printConstraints(const PQL::SimplificationContext& context, glp_prob* lp){
+            
+            if(context.getPrintLevel() < 1)
+                return;
+
+            int nCols = glp_get_num_cols(lp);
+            int nRows = glp_get_num_rows(lp);
+            
+            std::vector<int> indices(nCols + 1);
+            std::vector<double> coef(nCols + 1);
+            int l;
+
+            auto nt = context.net()->numberOfTransitions();
+
+            for(int i = 1; i <= nRows; i++){
+                l = glp_get_mat_row(lp, i, indices.data(), coef.data());
+                std::cout << "Row " << i << "[len: " << l << "]: ";
+
+                bool first_print = true;
+                for(int j = 1; j <= l; j++){
+                    if(!first_print) std::cout << " + ";
+                    if((indices[j] - 1) < nt){
+                        std::cout << coef[j] << "*t" << (indices[j] - 1) / nt << "." << *context.net()->transitionNames()[(indices[j] - 1) % nt];
+                    }else{
+                        std::cout << coef[j] << "*" << glp_get_col_name(lp, indices[j]);
+                    }
+                    first_print = false;
+                }
+
+                if(first_print){
+                    std::cout << "<empty-row>";
+                }
+                
+
+                double up = glp_get_row_ub(lp, i);
+                double lb = glp_get_row_lb(lp, i);
+                switch(glp_get_row_type(lp, i)){
+                    case GLP_FR:
+                        std::cout << " is unconstraint";
+                        break;
+                    case GLP_LO:
+                        std::cout << " >= " << bound_or_inf(lb);
+                        break;
+                    case GLP_UP:
+                        std::cout << " <= " << bound_or_inf(up);
+                        break;
+                    case GLP_DB:
+                        std::cout << " in [" << bound_or_inf(lb) << ", " << bound_or_inf(up) << "]";
+                        break;
+                    case GLP_FX:
+                        std::cout << " = " << bound_or_inf(lb);
+                        break;
+                }
+                std::cout << "\n";
+            }
+            
+        }
+
         bool LinearProgram::isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime) {
             bool use_ilp = true;
             auto net = context.net();
@@ -118,6 +182,8 @@ namespace PetriEngine {
                 glp_set_col_bnds(lp, i, GLP_LO, 0, infty);
             }
 
+            printConstraints(context, lp);
+
             // Minimize the objective
             glp_set_obj_dir(lp, GLP_MIN);
             auto stime = glp_time();
diff --git a/src/PetriEngine/Simplification/LinearPrograms.cpp b/src/PetriEngine/Simplification/LinearPrograms.cpp
index a8c311a37..104052e71 100644
--- a/src/PetriEngine/Simplification/LinearPrograms.cpp
+++ b/src/PetriEngine/Simplification/LinearPrograms.cpp
@@ -12,7 +12,10 @@ namespace PetriEngine {
         bool AbstractProgramCollection::satisfiable(const PQL::SimplificationContext& context, uint32_t solvetime)
         {
             reset();
-            if (context.timeout() || has_empty || solvetime == 0) return true;
+            if (context.timeout() || has_empty || solvetime == 0){ 
+                std::cout << "returning from timeout/empty\n";
+                return true;
+            }
             if (_result != UNKNOWN)
             {
                 if (_result == IMPOSSIBLE)
@@ -154,8 +157,9 @@ namespace PetriEngine {
 
         bool MergeCollection::merge(bool& has_empty, LinearProgram& program, bool dry_run)
         {
-            if (program.knownImpossible())
+            if (program.knownImpossible()) {
                 return false;
+            }
 
             bool lempty = false;
             bool more_left;
@@ -172,17 +176,21 @@ namespace PetriEngine {
                     left->reset();
                     merge_right = false;
                 }
+                
                 ++curr;
                 assert(curr <= _size);
+
                 more_left = left->merge(lempty, prog/*, dry_run || curr < nsat*/);
                 if (!more_left) merge_right = true;
-                if (curr >= nsat || !(more_left || more_right))
+                if (curr > nsat || !(more_left || more_right))
                 {
-                    if ((!dry_run && prog.knownImpossible()) && (more_left || more_right))
+                    if ((!dry_run && prog.knownImpossible()) && (more_left || more_right)) {
                         continue;
+                    }
 
-                    if (!dry_run)
+                    if (!dry_run) {
                         program.swap(prog);
+                    }
 
                     break;
                 }
diff --git a/src/PetriEngine/options.cpp b/src/PetriEngine/options.cpp
index f5379408d..d9d8e9fa7 100644
--- a/src/PetriEngine/options.cpp
+++ b/src/PetriEngine/options.cpp
@@ -110,6 +110,17 @@ void options_t::print(std::ostream& optionsOut) {
 
     optionsOut << ",LPSolve_Timeout=" << lpsolveTimeout;
 
+    switch(lpPrintLevel){
+        case 0:
+            optionsOut << ",LP_Print=DISABLED";
+            break;
+        case 1:
+            optionsOut << ",LP_Print=Constraints";
+            break;
+        default:
+            optionsOut << ",LP_Print=Full";
+    }
+
 
     if (usedctl) {
         if (ctlalgorithm == CTL::CZero) {
@@ -185,6 +196,10 @@ void printHelp() {
         "                                       write --interval-timeout 0 to disable interval limits\n"
         "  --partition-timeout <timeout>        Timeout for color partitioning in seconds (default 5)\n"
         "  -l, --lpsolve-timeout <timeout>      LPSolve timeout in seconds, default 10\n"
+        "  -lpp, --lp-print <level>             LP diagnostic print level\n"
+        "                                       - 0 disabled (default)\n"
+        "                                       - 1 constraints only\n"
+        "                                       - 2 constraints and solutions}\n"
         "  -p, --disable-partial-order          Disable partial order reduction (stubborn sets)\n"
         "  --ltl-por <type>                     Select partial order method to use with LTL engine (default automaton).\n"
         "                                       - automaton  apply Büchi-guided stubborn set method (Jensen et al., 2021).\n"
@@ -374,6 +389,13 @@ bool options_t::parse(int argc, const char** argv) {
             if (sscanf(argv[++i], "%d", &lpsolveTimeout) != 1 || lpsolveTimeout < 0) {
                 throw base_error("Argument Error: Invalid LPSolve timeout argument ", std::quoted(argv[i]));
             }
+        } else if (std::strcmp(argv[i], "-lpp") == 0 || std::strcmp(argv[i], "--lp-print") == 0){
+            if (i == argc - 1) {
+                throw base_error("Missing number after ", std::quoted(argv[i]));
+            }
+            if (sscanf(argv[++i], "%d", &lpPrintLevel) != 1 || lpPrintLevel < 0) {
+                throw base_error("Argument Error: Invalid lpPrintLevel argument ", std::quoted(argv[i]));
+            }
         } else if (std::strcmp(argv[i], "-e") == 0 || std::strcmp(argv[i], "--state-space-exploration") == 0) {
             statespaceexploration = true;
             computePartition = false;
diff --git a/src/PetriParse/PNMLParser.cpp b/src/PetriParse/PNMLParser.cpp
index 819246f9f..bc00dd66e 100644
--- a/src/PetriParse/PNMLParser.cpp
+++ b/src/PetriParse/PNMLParser.cpp
@@ -592,6 +592,44 @@ ArcExpression_ptr PNMLParser::parseNumberOfExpression(rapidxml::xml_node<>* elem
         return std::make_shared<AddExpression>(std::move(result));
 }
 
+void PNMLParser::parseMarking(const rapidxml::xml_document<>& doc, PetriEngine::AbstractPetriNetBuilder* builder,
+    ColorTypeMap* colorTypes)
+{
+    this->colorTypes = *colorTypes;
+    this->builder = builder;
+
+    rapidxml::xml_node<>* root = doc.first_node();
+    if(strcmp(root->name(), "marking") != 0)
+    {
+        throw base_error("expected marking tag, got ", root->name());
+    }
+
+    for (auto child = root->first_node(); child != nullptr; child = child->next_sibling())
+    {
+        if (strcmp(child->name(), "place") != 0)
+        {
+            throw base_error("expected only place tags in marking, got ", child->name());
+        }
+
+        const auto idAttribute = child->first_attribute("id");
+
+        if (idAttribute == nullptr)
+        {
+            throw base_error("expected place to have id attribute");
+        }
+
+        std::string id = idAttribute->value();
+
+        std::unordered_map<const Variable*, const Color*> binding;
+        EquivalenceVec placePartition;
+        ExpressionContext context {binding, *colorTypes, placePartition};
+        auto ae = parseArcExpression(child->first_node());
+        auto initialMarking = EvaluationVisitor::evaluate(*ae, context);
+
+        builder->addTokens(std::move(id), std::move(initialMarking));
+    }
+}
+
 void PNMLParser::parseElement(rapidxml::xml_node<>* element) {
 
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
diff --git a/src/VerifyPN.cpp b/src/VerifyPN.cpp
index c669c2990..5b9d46727 100644
--- a/src/VerifyPN.cpp
+++ b/src/VerifyPN.cpp
@@ -443,6 +443,10 @@ Condition_ptr simplify_ltl_query(Condition_ptr query,
         out << std::endl;
     }
 
+    std::cout << "PushNegated: ";
+    cond->toString(std::cout);
+    std::cout << "\n";
+
     try {
         auto simp_cond = PetriEngine::PQL::simplify(cond, simplificationContext);
         cond = pushNegation(simp_cond.formula, stats, evalContext, names.size() > 1, false, true);
@@ -578,7 +582,7 @@ void simplify_queries(const MarkVal* marking,
                     if (options.logic == TemporalLogic::LTL) {
                         if (options.queryReductionTimeout == 0 || qt == 0) continue;
                         SimplificationContext simplificationContext(marking, net, qt,
-                            options.lpsolveTimeout, &cache);
+                            options.lpsolveTimeout, options.lpPrintLevel, &cache);
                         if (simplificationContext.markingOutOfBounds()) {
                             std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction for LTL is skipped.\n";
                             break;
@@ -609,7 +613,7 @@ void simplify_queries(const MarkVal* marking,
 
                     if (options.queryReductionTimeout > 0 && qt > 0) {  
                         SimplificationContext simplificationContext(marking, net, qt,
-                            options.lpsolveTimeout, &cache);
+                            options.lpsolveTimeout, options.lpPrintLevel, &cache);
                         if (simplificationContext.markingOutOfBounds()) {
                             std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction is skipped.\n";
                             break;
@@ -733,7 +737,7 @@ void initialize_potency(const MarkVal* marking,
 
                     if (options.initPotencyTimeout > 0 && pt > 0) {
                         SimplificationContext potencyInitializationContext(marking, net, pt,
-                                                                           options.lpsolveTimeout,
+                                                                           options.lpsolveTimeout, options.lpPrintLevel,
                                                                            &cache, options.initPotencyTimeout);
                         try {
                             uint32_t maxConfigurationsSolved = 10;