ar ex1 done

[master.git] / ar / assignments / src / 1.smt

diff --git a/ar/assignments/src/1.smt b/ar/assignments/src/1.smt
index 77871e1..cf5342e 100644 (file)
--- a/ar/assignments/src/1.smt
+++ b/ar/assignments/src/1.smt
@@ -31,11 +31,6 @@
        (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
        (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
 
-       (= (+ t1n t2n t3n t4n t5n t6n) 4)
-       (= (+ t1s t2s t3s t4s t5s t6s) 8)
-       (= (+ t1c t2c t3c t4c t5c t6c) 10)
-       (= (+ t1d t2d t3d t4d t5d t6d) 5)
-
        (or (= 0 t1p) (= 0 t1c))
        (or (= 0 t2p) (= 0 t2c))
        (or (= 0 t3p) (= 0 t3c))
@@ -43,11 +38,6 @@
        (or (= 0 t5p) (= 0 t5c))
        (or (= 0 t6p) (= 0 t6c))
 
-       (= t3s 0)
-       (= t4s 0)
-       (= t5s 0)
-       (= t6s 0)
-
        (<= t1d 1)
        (<= t2d 1)
        (<= t3d 1)
@@ -55,6 +45,16 @@
        (<= t5d 1)
        (<= t6d 1)
 
+       (= t3s 0)
+       (= t4s 0)
+       (= t5s 0)
+       (= t6s 0)
+
+       (= (+ t1n t2n t3n t4n t5n t6n) 4)
+       (= (+ t1s t2s t3s t4s t5s t6s) 8)
+       (= (+ t1c t2c t3c t4c t5c t6c) 10)
+       (= (+ t1d t2d t3d t4d t5d t6d) 5)
+
        (>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
 )
 )