unknown

Initial ITS

Start location: l4
Program variables: c0^0 deltaext^0 deltaext_new^0 wnt^0
   0: l0 -> l2 : c0^0'=c0^post1, deltaext^0'=deltaext^post1, deltaext_new^0'=deltaext_new^post1, wnt^0'=wnt^post1, (1+deltaext^0-deltaext_new^0 <= 0 /\ deltaext^0-deltaext^post1 == 0 /\ -deltaext_new^post1+deltaext_new^0 == 0 /\ c0^0-c0^post1 == 0 /\ -wnt^post1+wnt^0 == 0), cost: 1
   1: l0 -> l2 : c0^0'=c0^post2, deltaext^0'=deltaext^post2, deltaext_new^0'=deltaext_new^post2, wnt^0'=wnt^post2, (wnt^0-wnt^post2 == 0 /\ -deltaext^post2+deltaext^0 == 0 /\ 1-deltaext^0+deltaext_new^0 <= 0 /\ -deltaext_new^post2+deltaext_new^0 == 0 /\ c0^0-c0^post2 == 0), cost: 1
   2: l2 -> l1 : c0^0'=c0^post3, deltaext^0'=deltaext^post3, deltaext_new^0'=deltaext_new^post3, wnt^0'=wnt^post3, (-deltaext_new^post3+deltaext_new^0 == 0 /\ wnt^0-wnt^post3 == 0 /\ -c0^post3+c0^0 == 0 /\ deltaext^post3-deltaext_new^0 == 0), cost: 1
   3: l1 -> l0 : c0^0'=c0^post4, deltaext^0'=deltaext^post4, deltaext_new^0'=deltaext_new^post4, wnt^0'=wnt^post4, (-deltaext^post4+deltaext^0 == 0 /\ -deltaext^0+deltaext_new^post4 == 0 /\ -1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0 /\ -c0^post4+c0^0 == 0 /\ -wnt^post4+wnt^0 == 0), cost: 1
   4: l1 -> l0 : c0^0'=c0^post5, deltaext^0'=deltaext^post5, deltaext_new^0'=deltaext_new^post5, wnt^0'=wnt^post5, (2+c0^0+wnt^0-2*deltaext^0 <= 0 /\ c0^0-c0^post5 == 0 /\ deltaext^0-deltaext^post5 == 0 /\ -wnt^post5+wnt^0 == 0 /\ 1+deltaext_new^post5-deltaext^0 == 0), cost: 1
   5: l1 -> l0 : c0^0'=c0^post6, deltaext^0'=deltaext^post6, deltaext_new^0'=deltaext_new^post6, wnt^0'=wnt^post6, (c0^0-c0^post6 == 0 /\ deltaext^0-deltaext^post6 == 0 /\ wnt^0-wnt^post6 == 0 /\ 1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ -1+deltaext_new^post6-deltaext^0 == 0), cost: 1
   6: l3 -> l1 : c0^0'=c0^post7, deltaext^0'=deltaext^post7, deltaext_new^0'=deltaext_new^post7, wnt^0'=wnt^post7, (-wnt^0 <= 0 /\ -deltaext_new^post7+deltaext_new^0 == 0 /\ -2+c0^post7 == 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -deltaext^post7+deltaext^0 == 0 /\ -3+wnt^0 <= 0 /\ wnt^0-wnt^post7 == 0), cost: 1
   7: l4 -> l3 : c0^0'=c0^post8, deltaext^0'=deltaext^post8, deltaext_new^0'=deltaext_new^post8, wnt^0'=wnt^post8, (-wnt^post8+wnt^0 == 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0), cost: 1

Chained Linear Paths

Start location: l4
Program variables: c0^0 deltaext^0 deltaext_new^0 wnt^0
   0: l0 -> l2 : c0^0'=c0^post1, deltaext^0'=deltaext^post1, deltaext_new^0'=deltaext_new^post1, wnt^0'=wnt^post1, (1+deltaext^0-deltaext_new^0 <= 0 /\ deltaext^0-deltaext^post1 == 0 /\ -deltaext_new^post1+deltaext_new^0 == 0 /\ c0^0-c0^post1 == 0 /\ -wnt^post1+wnt^0 == 0), cost: 1
   1: l0 -> l2 : c0^0'=c0^post2, deltaext^0'=deltaext^post2, deltaext_new^0'=deltaext_new^post2, wnt^0'=wnt^post2, (wnt^0-wnt^post2 == 0 /\ -deltaext^post2+deltaext^0 == 0 /\ 1-deltaext^0+deltaext_new^0 <= 0 /\ -deltaext_new^post2+deltaext_new^0 == 0 /\ c0^0-c0^post2 == 0), cost: 1
   2: l2 -> l1 : c0^0'=c0^post3, deltaext^0'=deltaext^post3, deltaext_new^0'=deltaext_new^post3, wnt^0'=wnt^post3, (-deltaext_new^post3+deltaext_new^0 == 0 /\ wnt^0-wnt^post3 == 0 /\ -c0^post3+c0^0 == 0 /\ deltaext^post3-deltaext_new^0 == 0), cost: 1
   3: l1 -> l0 : c0^0'=c0^post4, deltaext^0'=deltaext^post4, deltaext_new^0'=deltaext_new^post4, wnt^0'=wnt^post4, (-deltaext^post4+deltaext^0 == 0 /\ -deltaext^0+deltaext_new^post4 == 0 /\ -1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0 /\ -c0^post4+c0^0 == 0 /\ -wnt^post4+wnt^0 == 0), cost: 1
   4: l1 -> l0 : c0^0'=c0^post5, deltaext^0'=deltaext^post5, deltaext_new^0'=deltaext_new^post5, wnt^0'=wnt^post5, (2+c0^0+wnt^0-2*deltaext^0 <= 0 /\ c0^0-c0^post5 == 0 /\ deltaext^0-deltaext^post5 == 0 /\ -wnt^post5+wnt^0 == 0 /\ 1+deltaext_new^post5-deltaext^0 == 0), cost: 1
   5: l1 -> l0 : c0^0'=c0^post6, deltaext^0'=deltaext^post6, deltaext_new^0'=deltaext_new^post6, wnt^0'=wnt^post6, (c0^0-c0^post6 == 0 /\ deltaext^0-deltaext^post6 == 0 /\ wnt^0-wnt^post6 == 0 /\ 1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ -1+deltaext_new^post6-deltaext^0 == 0), cost: 1
   8: l4 -> l1 : c0^0'=c0^post7, deltaext^0'=deltaext^post7, deltaext_new^0'=deltaext_new^post7, wnt^0'=wnt^post7, (-3+deltaext^post8 <= 0 /\ -wnt^post8+wnt^0 == 0 /\ -wnt^post8 <= 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -2+c0^post7 == 0 /\ -deltaext^post7+deltaext^post8 == 0 /\ -deltaext_new^post7+deltaext_new^post8 == 0 /\ -3+wnt^post8 <= 0 /\ wnt^post8-wnt^post7 == 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0 /\ -deltaext^post8 <= 0), cost: 1

	Eliminating location l3 by chaining:

	Applied chaining

	First rule:
	l4 -> l3 : c0^0'=c0^post8, deltaext^0'=deltaext^post8, deltaext_new^0'=deltaext_new^post8, wnt^0'=wnt^post8, (-wnt^post8+wnt^0 == 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0), cost: 1
	Second rule:
	l3 -> l1 : c0^0'=c0^post7, deltaext^0'=deltaext^post7, deltaext_new^0'=deltaext_new^post7, wnt^0'=wnt^post7, (-wnt^0 <= 0 /\ -deltaext_new^post7+deltaext_new^0 == 0 /\ -2+c0^post7 == 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -deltaext^post7+deltaext^0 == 0 /\ -3+wnt^0 <= 0 /\ wnt^0-wnt^post7 == 0), cost: 1
	New rule:
	l4 -> l1 : c0^0'=c0^post7, deltaext^0'=deltaext^post7, deltaext_new^0'=deltaext_new^post7, wnt^0'=wnt^post7, (-3+deltaext^post8 <= 0 /\ -wnt^post8+wnt^0 == 0 /\ -wnt^post8 <= 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -2+c0^post7 == 0 /\ -deltaext^post7+deltaext^post8 == 0 /\ -deltaext_new^post7+deltaext_new^post8 == 0 /\ -3+wnt^post8 <= 0 /\ wnt^post8-wnt^post7 == 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0 /\ -deltaext^post8 <= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 6 7

Simplified Transitions

Start location: l4
Program variables: c0^0 deltaext^0 deltaext_new^0 wnt^0
   9: l0 -> l2 : 1+deltaext^0-deltaext_new^0 <= 0, cost: 1
  10: l0 -> l2 : 1-deltaext^0+deltaext_new^0 <= 0, cost: 1
  11: l2 -> l1 : deltaext^0'=deltaext_new^0, T, cost: 1
  12: l1 -> l0 : deltaext_new^0'=deltaext^0, (-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
  13: l1 -> l0 : deltaext_new^0'=-1+deltaext^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
  14: l1 -> l0 : deltaext_new^0'=1+deltaext^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
  15: l4 -> l1 : c0^0'=2, (-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l2 : c0^0'=c0^post1, deltaext^0'=deltaext^post1, deltaext_new^0'=deltaext_new^post1, wnt^0'=wnt^post1, (1+deltaext^0-deltaext_new^0 <= 0 /\ deltaext^0-deltaext^post1 == 0 /\ -deltaext_new^post1+deltaext_new^0 == 0 /\ c0^0-c0^post1 == 0 /\ -wnt^post1+wnt^0 == 0), cost: 1
	New rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (0 == 0 /\ 1+deltaext^0-deltaext_new^0 <= 0), cost: 1
	
		propagated equality deltaext^post1 = deltaext^0
		
		propagated equality deltaext_new^post1 = deltaext_new^0
		
		propagated equality c0^post1 = c0^0
		
		propagated equality wnt^post1 = wnt^0
		
	Simplified Guard

	Original rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (0 == 0 /\ 1+deltaext^0-deltaext_new^0 <= 0), cost: 1
	New rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, 1+deltaext^0-deltaext_new^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, 1+deltaext^0-deltaext_new^0 <= 0, cost: 1
	New rule:
	l0 -> l2 : 1+deltaext^0-deltaext_new^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l2 : c0^0'=c0^post2, deltaext^0'=deltaext^post2, deltaext_new^0'=deltaext_new^post2, wnt^0'=wnt^post2, (wnt^0-wnt^post2 == 0 /\ -deltaext^post2+deltaext^0 == 0 /\ 1-deltaext^0+deltaext_new^0 <= 0 /\ -deltaext_new^post2+deltaext_new^0 == 0 /\ c0^0-c0^post2 == 0), cost: 1
	New rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (0 == 0 /\ 1-deltaext^0+deltaext_new^0 <= 0), cost: 1
	
		propagated equality wnt^post2 = wnt^0
		
		propagated equality deltaext^post2 = deltaext^0
		
		propagated equality deltaext_new^post2 = deltaext_new^0
		
		propagated equality c0^post2 = c0^0
		
	Simplified Guard

	Original rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (0 == 0 /\ 1-deltaext^0+deltaext_new^0 <= 0), cost: 1
	New rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, 1-deltaext^0+deltaext_new^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l2 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, 1-deltaext^0+deltaext_new^0 <= 0, cost: 1
	New rule:
	l0 -> l2 : 1-deltaext^0+deltaext_new^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l1 : c0^0'=c0^post3, deltaext^0'=deltaext^post3, deltaext_new^0'=deltaext_new^post3, wnt^0'=wnt^post3, (-deltaext_new^post3+deltaext_new^0 == 0 /\ wnt^0-wnt^post3 == 0 /\ -c0^post3+c0^0 == 0 /\ deltaext^post3-deltaext_new^0 == 0), cost: 1
	New rule:
	l2 -> l1 : c0^0'=c0^0, deltaext^0'=deltaext_new^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, 0 == 0, cost: 1
	
		propagated equality deltaext_new^post3 = deltaext_new^0
		
		propagated equality wnt^post3 = wnt^0
		
		propagated equality c0^post3 = c0^0
		
		propagated equality deltaext^post3 = deltaext_new^0
		
	Simplified Guard

	Original rule:
	l2 -> l1 : c0^0'=c0^0, deltaext^0'=deltaext_new^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, 0 == 0, cost: 1
	New rule:
	l2 -> l1 : c0^0'=c0^0, deltaext^0'=deltaext_new^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l1 : c0^0'=c0^0, deltaext^0'=deltaext_new^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, T, cost: 1
	New rule:
	l2 -> l1 : deltaext^0'=deltaext_new^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l0 : c0^0'=c0^post4, deltaext^0'=deltaext^post4, deltaext_new^0'=deltaext_new^post4, wnt^0'=wnt^post4, (-deltaext^post4+deltaext^0 == 0 /\ -deltaext^0+deltaext_new^post4 == 0 /\ -1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0 /\ -c0^post4+c0^0 == 0 /\ -wnt^post4+wnt^0 == 0), cost: 1
	New rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext^0, wnt^0'=wnt^0, (0 == 0 /\ -1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	
		propagated equality deltaext^post4 = deltaext^0
		
		propagated equality deltaext_new^post4 = deltaext^0
		
		propagated equality c0^post4 = c0^0
		
		propagated equality wnt^post4 = wnt^0
		
	Simplified Guard

	Original rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext^0, wnt^0'=wnt^0, (0 == 0 /\ -1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext^0, wnt^0'=wnt^0, (-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext^0, wnt^0'=wnt^0, (-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : deltaext_new^0'=deltaext^0, (-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l0 : c0^0'=c0^post5, deltaext^0'=deltaext^post5, deltaext_new^0'=deltaext_new^post5, wnt^0'=wnt^post5, (2+c0^0+wnt^0-2*deltaext^0 <= 0 /\ c0^0-c0^post5 == 0 /\ deltaext^0-deltaext^post5 == 0 /\ -wnt^post5+wnt^0 == 0 /\ 1+deltaext_new^post5-deltaext^0 == 0), cost: 1
	New rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=-1+deltaext^0, wnt^0'=wnt^0, (0 == 0 /\ 2+c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	
		propagated equality c0^post5 = c0^0
		
		propagated equality deltaext^post5 = deltaext^0
		
		propagated equality wnt^post5 = wnt^0
		
		propagated equality deltaext_new^post5 = -1+deltaext^0
		
	Simplified Guard

	Original rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=-1+deltaext^0, wnt^0'=wnt^0, (0 == 0 /\ 2+c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=-1+deltaext^0, wnt^0'=wnt^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=-1+deltaext^0, wnt^0'=wnt^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
	New rule:
	l1 -> l0 : deltaext_new^0'=-1+deltaext^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l0 : c0^0'=c0^post6, deltaext^0'=deltaext^post6, deltaext_new^0'=deltaext_new^post6, wnt^0'=wnt^post6, (c0^0-c0^post6 == 0 /\ deltaext^0-deltaext^post6 == 0 /\ wnt^0-wnt^post6 == 0 /\ 1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ -1+deltaext_new^post6-deltaext^0 == 0), cost: 1
	New rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=1+deltaext^0, wnt^0'=wnt^0, (0 == 0 /\ 1-c0^0-wnt^0+2*deltaext^0 <= 0), cost: 1
	
		propagated equality c0^post6 = c0^0
		
		propagated equality deltaext^post6 = deltaext^0
		
		propagated equality wnt^post6 = wnt^0
		
		propagated equality deltaext_new^post6 = 1+deltaext^0
		
	Simplified Guard

	Original rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=1+deltaext^0, wnt^0'=wnt^0, (0 == 0 /\ 1-c0^0-wnt^0+2*deltaext^0 <= 0), cost: 1
	New rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=1+deltaext^0, wnt^0'=wnt^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l0 : c0^0'=c0^0, deltaext^0'=deltaext^0, deltaext_new^0'=1+deltaext^0, wnt^0'=wnt^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
	New rule:
	l1 -> l0 : deltaext_new^0'=1+deltaext^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l1 : c0^0'=c0^post7, deltaext^0'=deltaext^post7, deltaext_new^0'=deltaext_new^post7, wnt^0'=wnt^post7, (-3+deltaext^post8 <= 0 /\ -wnt^post8+wnt^0 == 0 /\ -wnt^post8 <= 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -2+c0^post7 == 0 /\ -deltaext^post7+deltaext^post8 == 0 /\ -deltaext_new^post7+deltaext_new^post8 == 0 /\ -3+wnt^post8 <= 0 /\ wnt^post8-wnt^post7 == 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0 /\ -deltaext^post8 <= 0), cost: 1
	New rule:
	l4 -> l1 : c0^0'=2, deltaext^0'=deltaext^post8, deltaext_new^0'=deltaext_new^post8, wnt^0'=wnt^post8, (0 == 0 /\ -3+deltaext^post8 <= 0 /\ -wnt^post8+wnt^0 == 0 /\ -wnt^post8 <= 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -3+wnt^post8 <= 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0 /\ -deltaext^post8 <= 0), cost: 1
	
		propagated equality c0^post7 = 2
		
		propagated equality deltaext^post7 = deltaext^post8
		
		propagated equality deltaext_new^post7 = deltaext_new^post8
		
		propagated equality wnt^post7 = wnt^post8
		
	Propagated Equalities

	Original rule:
	l4 -> l1 : c0^0'=2, deltaext^0'=deltaext^post8, deltaext_new^0'=deltaext_new^post8, wnt^0'=wnt^post8, (0 == 0 /\ -3+deltaext^post8 <= 0 /\ -wnt^post8+wnt^0 == 0 /\ -wnt^post8 <= 0 /\ -deltaext_new^post8+deltaext_new^0 == 0 /\ -3+wnt^post8 <= 0 /\ -deltaext^post8+deltaext^0 == 0 /\ -c0^post8+c0^0 == 0 /\ -deltaext^post8 <= 0), cost: 1
	New rule:
	l4 -> l1 : c0^0'=2, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (0 == 0 /\ -wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1
	
		propagated equality wnt^post8 = wnt^0
		
		propagated equality deltaext_new^post8 = deltaext_new^0
		
		propagated equality deltaext^post8 = deltaext^0
		
		propagated equality c0^post8 = c0^0
		
	Simplified Guard

	Original rule:
	l4 -> l1 : c0^0'=2, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (0 == 0 /\ -wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1
	New rule:
	l4 -> l1 : c0^0'=2, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l1 : c0^0'=2, deltaext^0'=deltaext^0, deltaext_new^0'=deltaext_new^0, wnt^0'=wnt^0, (-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1
	New rule:
	l4 -> l1 : c0^0'=2, (-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1

Step with 15

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)]
	
	Blocked

	[{}, {}]

Step with 12

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 12[(-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)]
	
	Blocked

	[{}, {12[T]}]

Step with 13

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {}]

Step with 10

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {9[T]}, {}]

Step with 11

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)], 11[T]
	
	Blocked

	[{}, {12[T]}, {9[T]}, {}, {}]

Accelerate

Start location: l4
Program variables: c0^0 deltaext^0 deltaext_new^0 wnt^0
   9: l0 -> l2 : 1+deltaext^0-deltaext_new^0 <= 0, cost: 1
  10: l0 -> l2 : 1-deltaext^0+deltaext_new^0 <= 0, cost: 1
  11: l2 -> l1 : deltaext^0'=deltaext_new^0, T, cost: 1
  12: l1 -> l0 : deltaext_new^0'=deltaext^0, (-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
  13: l1 -> l0 : deltaext_new^0'=-1+deltaext^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
  14: l1 -> l0 : deltaext_new^0'=1+deltaext^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
  16: l1 -> l1 : deltaext^0'=-n+deltaext^0, deltaext_new^0'=-n+deltaext^0, (-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0), cost: 1
  15: l4 -> l1 : c0^0'=2, (-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : deltaext^0'=-1+deltaext^0, deltaext_new^0'=-1+deltaext^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
	New rule:
	l1 -> l1 : deltaext^0'=-n+deltaext^0, deltaext_new^0'=-n+deltaext^0, (-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0), cost: 1

		-2-c0^0-wnt^0+2*deltaext^0 >= 0 [0]: montonic decrease yields -2*n-c0^0-wnt^0+2*deltaext^0 >= 0
		
		-2-c0^0-wnt^0+2*deltaext^0 >= 0 [1]: eventual increase yields (2 <= 0 /\ -2-c0^0-wnt^0+2*deltaext^0 >= 0)
		
		Replacement map: {-2-c0^0-wnt^0+2*deltaext^0 >= 0 -> -2*n-c0^0-wnt^0+2*deltaext^0 >= 0}

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)]
	
	Blocked

	[{}, {12[T]}, {16[T]}]

Step with 12

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)], 12[(-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {16[T]}, {}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 16[T]}]

Step with 13

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 16[T]}, {}]

Step with 10

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 16[T]}, {}, {}]

Step with 11

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)], 11[T]
	
	Blocked

	[{}, {12[T]}, {12[T], 16[T]}, {}, {}, {}]

Covered

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 16[T]}, {}, {11[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 16[T]}, {10[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 16[(-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0)]
	
	Blocked

	[{}, {12[T]}, {12[T], 13[T], 16[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)]
	
	Blocked

	[{}, {12[T], 16[T]}]

Step with 13

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 16[T]}, {}]

Step with 10

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 16[T]}, {}, {}]

Step with 11

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)], 11[T]
	
	Blocked

	[{}, {12[T], 16[T]}, {}, {}, {}]

Covered

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)], 10[(1-deltaext^0+deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 16[T]}, {}, {11[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 13[(2+c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 16[T]}, {10[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}]

Step with 14

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {}]

Step with 9

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {10[T]}, {}]

Step with 11

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)], 11[T]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {10[T]}, {}, {}]

Accelerate

Start location: l4
Program variables: c0^0 deltaext^0 deltaext_new^0 wnt^0
   9: l0 -> l2 : 1+deltaext^0-deltaext_new^0 <= 0, cost: 1
  10: l0 -> l2 : 1-deltaext^0+deltaext_new^0 <= 0, cost: 1
  11: l2 -> l1 : deltaext^0'=deltaext_new^0, T, cost: 1
  12: l1 -> l0 : deltaext_new^0'=deltaext^0, (-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0), cost: 1
  13: l1 -> l0 : deltaext_new^0'=-1+deltaext^0, 2+c0^0+wnt^0-2*deltaext^0 <= 0, cost: 1
  14: l1 -> l0 : deltaext_new^0'=1+deltaext^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
  16: l1 -> l1 : deltaext^0'=-n+deltaext^0, deltaext_new^0'=-n+deltaext^0, (-1+n >= 0 /\ -2*n-c0^0-wnt^0+2*deltaext^0 >= 0), cost: 1
  17: l1 -> l1 : deltaext^0'=n2+deltaext^0, deltaext_new^0'=n2+deltaext^0, (1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0), cost: 1
  15: l4 -> l1 : c0^0'=2, (-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0), cost: 1

	Loop Acceleration

	Original rule:
	l1 -> l1 : deltaext^0'=1+deltaext^0, deltaext_new^0'=1+deltaext^0, 1-c0^0-wnt^0+2*deltaext^0 <= 0, cost: 1
	New rule:
	l1 -> l1 : deltaext^0'=n2+deltaext^0, deltaext_new^0'=n2+deltaext^0, (1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0), cost: 1

		-1+c0^0+wnt^0-2*deltaext^0 >= 0 [0]: montonic decrease yields 1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0
		
		-1+c0^0+wnt^0-2*deltaext^0 >= 0 [1]: eventual increase yields (2 <= 0 /\ -1+c0^0+wnt^0-2*deltaext^0 >= 0)
		
		Replacement map: {-1+c0^0+wnt^0-2*deltaext^0 >= 0 -> 1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0}

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {17[T]}]

Step with 12

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)], 12[(-1-c0^0-wnt^0+2*deltaext^0 <= 0 /\ c0^0+wnt^0-2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {17[T]}, {}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 17[T]}]

Step with 14

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 13[T], 17[T]}, {}]

Step with 9

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 13[T], 17[T]}, {}, {}]

Step with 11

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)], 11[T]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 13[T], 17[T]}, {}, {}, {}]

Covered

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 13[T], 17[T]}, {}, {11[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 13[T], 17[T]}, {9[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 17[(1-2*n2+c0^0+wnt^0-2*deltaext^0 >= 0 /\ -1+n2 >= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T]}, {12[T], 13[T], 14[T], 17[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T], 17[T]}]

Step with 14

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T], 17[T]}, {}]

Step with 9

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T], 17[T]}, {}, {}]

Step with 11

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)], 11[T]
	
	Blocked

	[{}, {12[T], 13[T], 16[T], 17[T]}, {}, {}, {}]

Covered

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)], 9[(1+deltaext^0-deltaext_new^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T], 17[T]}, {}, {11[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)], 14[(1-c0^0-wnt^0+2*deltaext^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 16[T], 17[T]}, {9[T]}]

Backtrack

	Trace

	15[(-wnt^0 <= 0 /\ -deltaext^0 <= 0 /\ -3+deltaext^0 <= 0 /\ -3+wnt^0 <= 0)]
	
	Blocked

	[{}, {12[T], 13[T], 14[T], 16[T], 17[T]}]

Backtrack

	Trace

	Blocked

	[{15[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b