diff --git a/encodings/sas-sequential-incremental-multivalued-axioms-condeffects.lp b/encodings/sas-sequential-incremental-multivalued-axioms-condeffects.lp
new file mode 100644
index 0000000..5dad258
--- /dev/null
+++ b/encodings/sas-sequential-incremental-multivalued-axioms-condeffects.lp
@@ -0,0 +1,52 @@
+#include <incmode>.
+
+% Check feature requirements
+% :- requires(feature(actionCosts)).
+
+#program base.
+
+% Establish initial state
+holds(Variable, Value, 0) :- initialState(Variable, Value), not stateVariable(Variable).
+
+% Identify (head and) state variables
+headVariable(Rule,Variable) :- variable(Variable), axiomRule(Rule), postcondition(Rule,_,Variable,_).
+stateVariable(Variable)     :- headVariable(_,Variable).
+
+#program step(t). % t=1,2,...
+
+% Perform actions
+1 {occurs(Action, t) : action(Action)} 1.
+
+% Check preconditions
+:- occurs(Action, t), precondition(Action, Variable, Value), not holds(Variable, Value, t - 1).
+
+% Apply effects
+caused(Variable, Value, t) :- occurs(Action, t), postcondition(Action, Effect, Variable, Value),
+		  	      holds(Variable', Value', t) : precondition(Effect, Variable', Value').
+modified(Variable, t) :- caused(Variable, Value, t).
+
+holds(Variable, Value, t) :- caused(Variable, Value, t).
+holds(Variable, Value, t) :- holds(Variable, Value, t - 1), not modified(Variable, t).
+
+#program check(t). % t=0,1,...
+
+% Check that variables have unique values
+:- variable(Variable), {holds(Variable, Value, t) : contains(Variable, Value)} != 1.
+
+% Check mutexes
+:- mutexGroup(MutexGroup),  {holds(Variable, Value, t) : contains(MutexGroup, Variable, Value)} > 1.
+
+% Apply axioms
+derived(Variable, Value, t) :- axiomRule(Rule), postcondition(Rule,_,Variable,Value),
+		  	       holds(Variable', Value', t) : precondition(Rule, Variable', Value'), not headVariable(Rule,Variable').
+
+modified(Variable, t) :- derived(Variable, Value, t).
+
+holds(Variable, Value, t) :-      derived(Variable, Value, t), stateVariable(Variable).
+holds(Variable, Value, t) :- not modified(Variable,        t), stateVariable(Variable), initialState(Variable, Value).
+
+% Verify that goal is met
+:- query(t), goal(Variable, Value), not holds(Variable, Value, t).
+
+#show occurs/2.
+% #show holds/3.