(<= (+ (* 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))
(or (= 0 t5p) (= 0 t5c))
(or (= 0 t6p) (= 0 t6c))
- (= t3s 0)
- (= t4s 0)
- (= t5s 0)
- (= t6s 0)
-
(<= t1d 1)
(<= t2d 1)
(<= t3d 1)
(<= 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>)
)
)