diff --git a/libyul/optimiser/KnowledgeBase.cpp b/libyul/optimiser/KnowledgeBase.cpp
index e0efdb17b..2c13ac05b 100644
--- a/libyul/optimiser/KnowledgeBase.cpp
+++ b/libyul/optimiser/KnowledgeBase.cpp
@@ -20,12 +20,69 @@
 
 #include <libyul/optimiser/KnowledgeBase.h>
 
-using namespace yul;
+#include <libyul/AsmData.h>
+#include <libyul/Utilities.h>
+#include <libyul/optimiser/SimplificationRules.h>
+#include <libyul/optimiser/Semantics.h>
 
-bool KnowledgeBase::knownToBeDifferent(YulString, YulString) const
+#include <libdevcore/CommonData.h>
+
+using namespace yul;
+using namespace dev;
+
+bool KnowledgeBase::knownToBeDifferent(YulString _a, YulString _b)
 {
-	// TODO try to use the simplification rules together with the
+	// Try to use the simplification rules together with the
 	// current values to turn `sub(_a, _b)` into a nonzero constant.
 	// If that fails, try `eq(_a, _b)`.
+
+	Expression expr1 = simplify(FunctionCall{{}, {{}, "sub"_yulstring}, make_vector<Expression>(Identifier{{}, _a}, Identifier{{}, _b})});
+	if (expr1.type() == typeid(Literal))
+		return valueOfLiteral(boost::get<Literal>(expr1)) != 0;
+
+	Expression expr2 = simplify(FunctionCall{{}, {{}, "eq"_yulstring}, make_vector<Expression>(Identifier{{}, _a}, Identifier{{}, _b})});
+	if (expr2.type() == typeid(Literal))
+		return valueOfLiteral(boost::get<Literal>(expr2)) == 0;
+
 	return false;
 }
+
+bool KnowledgeBase::knownToBeDifferentByAtLeast32(YulString _a, YulString _b)
+{
+	// Try to use the simplification rules together with the
+	// current values to turn `sub(_a, _b)` into a constant whose absolute value is at least 32.
+
+	Expression expr1 = simplify(FunctionCall{{}, {{}, "sub"_yulstring}, make_vector<Expression>(Identifier{{}, _a}, Identifier{{}, _b})});
+	if (expr1.type() == typeid(Literal))
+	{
+		u256 val = valueOfLiteral(boost::get<Literal>(expr1));
+		return val >= 32 && val <= u256(0) - 32;
+	}
+
+	return false;
+}
+
+Expression KnowledgeBase::simplify(Expression _expression)
+{
+	bool startedRecursion = (m_recursionCounter == 0);
+	dev::ScopeGuard{[&] { if (startedRecursion) m_recursionCounter = 0; }};
+
+	if (startedRecursion)
+		m_recursionCounter = 100;
+	else if (m_recursionCounter == 1)
+		return _expression;
+	else
+		--m_recursionCounter;
+
+	if (_expression.type() == typeid(FunctionCall))
+		for (Expression& arg: boost::get<FunctionCall>(_expression).arguments)
+			arg = simplify(arg);
+	else if (_expression.type() == typeid(FunctionalInstruction))
+		for (Expression& arg: boost::get<FunctionalInstruction>(_expression).arguments)
+			arg = simplify(arg);
+
+	if (auto match = SimplificationRules::findFirstMatch(_expression, m_dialect, m_variableValues))
+		return simplify(match->action().toExpression(locationOf(_expression)));
+
+	return _expression;
+}
diff --git a/libyul/optimiser/KnowledgeBase.h b/libyul/optimiser/KnowledgeBase.h
index 369cee532..35e2d40ee 100644
--- a/libyul/optimiser/KnowledgeBase.h
+++ b/libyul/optimiser/KnowledgeBase.h
@@ -27,7 +27,7 @@
 namespace yul
 {
 
-class Dialect;
+struct Dialect;
 
 /**
  * Class that can answer questions about values of variables and their relations.
@@ -42,12 +42,16 @@ public:
 		m_variableValues(_variableValues)
 	{}
 
-	bool knownToBeDifferent(YulString _a, YulString _b) const;
+	bool knownToBeDifferent(YulString _a, YulString _b);
+	bool knownToBeDifferentByAtLeast32(YulString _a, YulString _b);
 	bool knownToBeEqual(YulString _a, YulString _b) const { return _a == _b; }
 
 private:
+	Expression simplify(Expression _expression);
+
 	Dialect const& m_dialect;
 	std::map<YulString, Expression const*> const& m_variableValues;
+	size_t m_recursionCounter = 0;
 };
 
 }
diff --git a/test/libyul/yulOptimizerTests/sloadResolver/second_store_with_delta.yul b/test/libyul/yulOptimizerTests/sloadResolver/second_store_with_delta.yul
new file mode 100644
index 000000000..5d50185ae
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/sloadResolver/second_store_with_delta.yul
@@ -0,0 +1,24 @@
+{
+    let x := calldataload(1)
+    let a := add(x, 10)
+    let b := add(x, 20)
+    sstore(a, 7)
+    // does not invalidate the first store, because the
+    // difference is a constant, even if the absolute
+    // values are unknown
+    sstore(b, 8)
+    mstore(sload(a), sload(b))
+}
+// ====
+// step: sloadResolver
+// ----
+// {
+//     let x := calldataload(1)
+//     let a := add(x, 10)
+//     let b := add(x, 20)
+//     let _4 := 7
+//     sstore(a, _4)
+//     let _5 := 8
+//     sstore(b, _5)
+//     mstore(_4, _5)
+// }