; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
;
; This is a benchmark demonstrating a nasty incremental bug in the UF
; symmetry breaker, now fixed.
;
(set-logic QF_UF)
(declare-fun _substvar_29615_ () Bool)
(declare-sort T 0)
(declare-fun incident_o (T T) Bool)
(declare-fun sK25 () T)
(declare-fun sK26 () T)
(declare-fun ordered_by (T T T) Bool)
(declare-fun sK21 (T T) T)
(declare-fun incident_c (T T) Bool)
(declare-fun between_o (T T T T) Bool)
(declare-fun start_point (T T) Bool)
(declare-fun sK12 (T T) T)
(declare-fun meet (T T T) Bool)
(declare-fun end_point (T T) Bool)
(declare-fun inner_point (T T) Bool)
(declare-fun part_of (T T) Bool)
(declare-fun open (T) Bool)
(declare-fun sK22 (T T) T)
(declare-fun sK19 (T) T)
(declare-fun sum (T T) T)
(declare-fun sK4 (T T T) T)
(declare-fun sK2 (T T) T)
(declare-fun sK3 (T T) T)
(declare-fun sK0 (T T) T)
(declare-fun sK1 (T T T) T)
(declare-fun sK24 () T)
(declare-fun iProver_c13 () T)
(declare-fun iProver_c41 () T)
(declare-fun iProver_c14 () T)
(assert (incident_o sK26 sK24))
(assert (not (ordered_by sK24 sK25 sK26)))
(assert (not (= sK25 sK26)))
(assert (start_point (sK19 sK24) sK24))
(check-sat)
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK24 sK25))) (or (= sK25 sK24) (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)))))
(assert (let ((_let_0 (sK12 iProver_c13 sK25))) (or (= sK25 iProver_c13) (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK25 sK24)) (end_point _let_0 sK25))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK25 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK25 sK24)) (end_point _let_0 sK24))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK25 iProver_c13)) (end_point _let_0 iProver_c13))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (incident_c (sK4 sK24 sK25 _let_0) sK25) (meet _let_0 sK25 sK24))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (incident_c (sK4 iProver_c13 sK25 _let_0) sK25) (meet _let_0 sK25 iProver_c13))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (meet _let_0 sK25 sK24) (incident_c (sK4 sK24 sK25 _let_0) sK24))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (meet _let_0 sK25 iProver_c13) (incident_c (sK4 iProver_c13 sK25 _let_0) iProver_c13))))
(assert (let ((_let_0 (sK4 sK24 sK25 (sK12 sK26 sK25)))) (or (not (incident_c (sK12 sK26 sK25) sK25)) (not (incident_c (sK12 sK26 sK25) sK24)) (meet (sK12 sK26 sK25) sK25 sK24) (not (end_point _let_0 sK25)) (not (end_point _let_0 sK24)))))
(assert (let ((_let_0 (sK4 iProver_c13 sK25 (sK12 sK26 sK25)))) (or (not (incident_c (sK12 sK26 sK25) sK25)) (not (incident_c (sK12 sK26 sK25) iProver_c13)) (meet (sK12 sK26 sK25) sK25 iProver_c13) (not (end_point _let_0 sK25)) (not (end_point _let_0 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (inner_point _let_0 sK25))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (part_of sK25 sK24))) (or (not (part_of sK24 sK24)) (not (incident_c _let_0 sK25)) _let_1 (not _let_1) (part_of sK24 sK25) (not (incident_c _let_0 sK24)) (not (end_point _let_0 sK24))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (part_of iProver_c13 iProver_c14)) (not (incident_c _let_0 sK25)) (part_of sK25 iProver_c13) (part_of iProver_c13 sK25) (not (incident_c _let_0 iProver_c13)) (not (part_of sK25 iProver_c14)) (not (end_point _let_0 iProver_c14)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (part_of (sK2 sK25 _let_0) sK25))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (part_of (sK3 sK25 _let_0) sK25))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (incident_c _let_0 (sK2 sK25 _let_0)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (incident_c _let_0 (sK3 sK25 _let_0)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (part_of (sK2 sK25 _let_0) (sK3 sK25 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (part_of (sK3 sK25 _let_0) (sK2 sK25 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK25 sK24)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK25 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK24 sK25)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum iProver_c13 sK25)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK0 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK0 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK12 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK12 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK12 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK0 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (part_of sK25 sK24)) (incident_c _let_0 sK24))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (part_of sK25 iProver_c13)) (incident_c _let_0 iProver_c13))))
(assert (or (part_of sK24 sK25) (not (incident_c (sK0 sK24 sK25) sK25))))
(assert (or (part_of iProver_c13 sK25) (not (incident_c (sK0 iProver_c13 sK25) sK25))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK12 sK24 sK26))) (or (= sK26 sK24) (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)))))
(assert (let ((_let_0 (sK12 iProver_c13 sK26))) (or (= sK26 iProver_c13) (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK26 sK24)) (end_point _let_0 sK26))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK26 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK26 sK24)) (end_point _let_0 sK24))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK26 iProver_c13)) (end_point _let_0 iProver_c13))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (incident_c (sK4 sK24 sK26 _let_0) sK26) (meet _let_0 sK26 sK24))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (incident_c (sK4 iProver_c13 sK26 _let_0) sK26) (meet _let_0 sK26 iProver_c13))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (meet _let_0 sK26 sK24) (incident_c (sK4 sK24 sK26 _let_0) sK24))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (meet _let_0 sK26 iProver_c13) (incident_c (sK4 iProver_c13 sK26 _let_0) iProver_c13))))
(assert (let ((_let_0 (sK4 sK24 sK26 (sK12 sK25 sK26)))) (or (not (incident_c (sK12 sK25 sK26) sK26)) (not (incident_c (sK12 sK25 sK26) sK24)) (meet (sK12 sK25 sK26) sK26 sK24) (not (end_point _let_0 sK26)) (not (end_point _let_0 sK24)))))
(assert (let ((_let_0 (sK4 iProver_c13 sK26 (sK12 sK25 sK26)))) (or (not (incident_c (sK12 sK25 sK26) sK26)) (not (incident_c (sK12 sK25 sK26) iProver_c13)) (meet (sK12 sK25 sK26) sK26 iProver_c13) (not (end_point _let_0 sK26)) (not (end_point _let_0 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (inner_point _let_0 sK26))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (part_of sK26 sK24))) (or (not (part_of sK24 sK24)) (not (incident_c _let_0 sK26)) (part_of sK24 sK26) _let_1 (not _let_1) (not (incident_c _let_0 sK24)) (not (end_point _let_0 sK24))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (part_of iProver_c13 iProver_c14)) (not (incident_c _let_0 sK26)) (part_of iProver_c13 sK26) (part_of sK26 iProver_c13) (not (incident_c _let_0 iProver_c13)) (not (part_of sK26 iProver_c14)) (not (end_point _let_0 iProver_c14)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (part_of (sK2 sK26 _let_0) sK26))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (part_of (sK3 sK26 _let_0) sK26))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (incident_c _let_0 (sK2 sK26 _let_0)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (incident_c _let_0 (sK3 sK26 _let_0)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (part_of (sK2 sK26 _let_0) (sK3 sK26 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (part_of (sK3 sK26 _let_0) (sK2 sK26 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK26 sK24)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK26 iProver_c13)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK24 sK26)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum iProver_c13 sK26)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK0 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK0 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK12 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK12 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK12 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK0 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (part_of sK26 sK24)) (incident_c _let_0 sK24))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (part_of sK26 iProver_c13)) (incident_c _let_0 iProver_c13))))
(assert (or (part_of sK24 sK26) (not (incident_c (sK0 sK24 sK26) sK26))))
(assert (or (part_of iProver_c13 sK26) (not (incident_c (sK0 iProver_c13 sK26) sK26))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK21 sK24 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK24 _let_0 _let_1)) (= sK25 sK24)))))
(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by iProver_c13 _let_0 _let_1)) (= sK25 iProver_c13)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 (sK22 sK26 sK25))) (incident_o _let_0 sK25))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (or (not (ordered_by sK25 (sK21 sK26 sK25) _let_0)) (incident_o _let_0 sK25))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 sK24)) (between_o sK25 _let_0 _let_1 sK24)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 iProver_c13)) (between_o sK25 _let_0 _let_1 iProver_c13)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 sK24)) (between_o sK25 sK24 _let_1 _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 iProver_c13)) (between_o sK25 iProver_c13 _let_1 _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK22 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c14 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
(assert (let ((_let_0 (sK22 iProver_c14 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 _let_0 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 _let_0) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 _let_0 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 _let_0) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (or (incident_c (sK1 _let_0 _let_0 _let_0) _let_0) (= (sum _let_0 _let_0) _let_0))))
(assert (let ((_let_0 (sK22 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 _let_0 sK24 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (incident_c _let_2 _let_0) (= (sum sK24 _let_0) _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c14 sK25))) (let ((_let_2 (sK1 _let_0 iProver_c13 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (incident_c _let_2 _let_0) (= (sum iProver_c13 _let_0) _let_1))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (let ((_let_2 (sK1 sK24 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (= (sum _let_1 sK24) _let_0))))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (= (sum _let_1 iProver_c13) _let_0))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 sK24 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum _let_0 sK24) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum _let_0 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 iProver_c14 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
(assert (let ((_let_0 (sK21 iProver_c14 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1)))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0)))))))
(assert (let ((_let_0 (sK21 sK24 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK24 _let_0 _let_1)) (= sK26 sK24)))))
(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by iProver_c13 _let_0 _let_1)) (= sK26 iProver_c13)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 (sK22 sK25 sK26))) (incident_o _let_0 sK26))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (or (not (ordered_by sK26 (sK21 sK25 sK26) _let_0)) (incident_o _let_0 sK26))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 sK24)) (between_o sK26 _let_0 _let_1 sK24)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 iProver_c13)) (between_o sK26 _let_0 _let_1 iProver_c13)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 sK24)) (between_o sK26 sK24 _let_1 _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 iProver_c13)) (between_o sK26 iProver_c13 _let_1 _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK22 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0)))))
(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK21 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c14 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
(assert (let ((_let_0 (sK22 iProver_c14 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 _let_0 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 _let_0) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 _let_0 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 _let_0) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (or (incident_c (sK1 _let_0 _let_0 _let_0) _let_0) (= (sum _let_0 _let_0) _let_0))))
(assert (let ((_let_0 (sK22 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 _let_0 sK24 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (incident_c _let_2 _let_0) (= (sum sK24 _let_0) _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c14 sK26))) (let ((_let_2 (sK1 _let_0 iProver_c13 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (incident_c _let_2 _let_0) (= (sum iProver_c13 _let_0) _let_1))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (let ((_let_2 (sK1 sK24 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (= (sum _let_1 sK24) _let_0))))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (= (sum _let_1 iProver_c13) _let_0))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 sK24 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum _let_0 sK24) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum _let_0 iProver_c13) _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 iProver_c14 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1))))))
(assert (let ((_let_0 (sK21 iProver_c14 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0)))))
(assert (or (= iProver_c13 iProver_c14) false false _substvar_29615_ false false))
(assert (or (not (incident_c sK24 sK24)) (not (meet sK24 sK25 sK24)) (not (incident_c sK24 sK25)) (end_point sK24 sK25)))
(assert (or (not (meet iProver_c14 sK25 iProver_c13)) (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (incident_c sK24 iProver_c13))))
(assert (or (not (incident_c sK24 sK24)) (end_point sK24 sK24) (not (meet sK24 sK25 sK24)) (not (incident_c sK24 sK25))))
(assert (or (not (meet iProver_c14 sK25 iProver_c13)) (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (end_point sK24 iProver_c13)))
(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (incident_c (sK4 sK24 sK25 sK24) sK25)))
(assert (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (incident_c (sK4 iProver_c13 sK25 sK24) sK25) (meet sK24 sK25 iProver_c13)))
(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (incident_c (sK4 sK24 sK25 sK24) sK24)))
(assert (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (meet sK24 sK25 iProver_c13) (incident_c (sK4 iProver_c13 sK25 sK24) iProver_c13)))
(assert (let ((_let_0 (sK4 sK24 sK25 sK24))) (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (not (end_point _let_0 sK25)) (not (end_point _let_0 sK24)))))
(assert (let ((_let_0 (sK4 iProver_c13 sK25 sK24))) (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (meet sK24 sK25 iProver_c13) (not (end_point _let_0 sK25)) (not (end_point _let_0 iProver_c13)))))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (inner_point sK24 sK25)))
(assert (let ((_let_0 (part_of sK25 sK24))) (or (not (incident_c sK24 sK24)) (not (part_of sK24 sK24)) (not (end_point sK24 sK24)) _let_0 (not _let_0) (part_of sK24 sK25) (not (incident_c sK24 sK25)))))
(assert (or (not (part_of iProver_c13 iProver_c14)) (part_of sK25 iProver_c13) (part_of iProver_c13 sK25) (not (part_of sK25 iProver_c14)) (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (not (end_point sK24 iProver_c14))))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (part_of (sK2 sK25 sK24) sK25)))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (part_of (sK3 sK25 sK24) sK25)))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (incident_c sK24 (sK2 sK25 sK24))))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (incident_c sK24 (sK3 sK25 sK24))))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (part_of (sK2 sK25 sK24) (sK3 sK25 sK24)))))
(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (part_of (sK3 sK25 sK24) (sK2 sK25 sK24)))))
(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK25 sK24))))
(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK25 iProver_c13))))
(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK24 sK25))))
(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum iProver_c13 sK25))))
(assert (or (incident_c sK24 sK24) (not (part_of sK25 sK24)) (not (incident_c sK24 sK25))))
(assert (or (not (part_of sK25 iProver_c13)) (not (incident_c sK24 sK25)) (incident_c sK24 iProver_c13)))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (or (not (incident_c sK24 sK24)) (not (meet sK24 sK26 sK24)) (not (incident_c sK24 sK26)) (end_point sK24 sK26)))
(assert (or (not (meet iProver_c14 sK26 iProver_c13)) (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (end_point sK24 sK26)))
(assert (or (not (incident_c sK24 sK24)) (end_point sK24 sK24) (not (meet sK24 sK26 sK24)) (not (incident_c sK24 sK26))))
(assert (or (not (meet iProver_c14 sK26 iProver_c13)) (not (incident_c sK24 iProver_c13)) (end_point sK24 iProver_c13) (not (incident_c sK24 sK26))))
(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (incident_c (sK4 sK24 sK26 sK24) sK26)))
(assert (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (incident_c (sK4 iProver_c13 sK26 sK24) sK26) (meet sK24 sK26 iProver_c13)))
(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (incident_c (sK4 sK24 sK26 sK24) sK24)))
(assert (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (meet sK24 sK26 iProver_c13) (incident_c (sK4 iProver_c13 sK26 sK24) iProver_c13)))
(assert (let ((_let_0 (sK4 sK24 sK26 sK24))) (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (not (end_point _let_0 sK26)) (not (end_point _let_0 sK24)))))
(assert (let ((_let_0 (sK4 iProver_c13 sK26 sK24))) (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (meet sK24 sK26 iProver_c13) (not (end_point _let_0 sK26)) (not (end_point _let_0 iProver_c13)))))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (inner_point sK24 sK26)))
(assert (let ((_let_0 (part_of sK26 sK24))) (or (not (incident_c sK24 sK24)) (not (part_of sK24 sK24)) (not (end_point sK24 sK24)) (part_of sK24 sK26) _let_0 (not _let_0) (not (incident_c sK24 sK26)))))
(assert (or (not (part_of iProver_c13 iProver_c14)) (part_of iProver_c13 sK26) (part_of sK26 iProver_c13) (not (part_of sK26 iProver_c14)) (not (incident_c sK24 iProver_c13)) (not (end_point sK24 iProver_c14)) (not (incident_c sK24 sK26))))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (part_of (sK2 sK26 sK24) sK26)))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (part_of (sK3 sK26 sK24) sK26)))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (incident_c sK24 (sK2 sK26 sK24))))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (incident_c sK24 (sK3 sK26 sK24))))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (not (part_of (sK2 sK26 sK24) (sK3 sK26 sK24)))))
(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (not (part_of (sK3 sK26 sK24) (sK2 sK26 sK24)))))
(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK26 sK24))))
(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK26 iProver_c13))))
(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK24 sK26))))
(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum iProver_c13 sK26))))
(assert (or (incident_c sK24 sK24) (not (part_of sK26 sK24)) (not (incident_c sK24 sK26))))
(assert (or (not (part_of sK26 iProver_c13)) (incident_c sK24 iProver_c13) (not (incident_c sK24 sK26))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (let ((_let_0 (sK1 sK24 sK24 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (= (sum sK24 sK24) sK25))))
(assert (let ((_let_0 (sK1 iProver_c13 iProver_c14 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c14)) (= (sum iProver_c14 iProver_c13) sK25))))
(assert (let ((_let_0 (sK1 sK24 sK24 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (= (sum sK24 sK24) sK26))))
(assert (let ((_let_0 (sK1 iProver_c13 iProver_c14 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c14)) (= (sum iProver_c14 iProver_c13) sK26))))
(assert (let ((_let_0 (sum sK24 sK24))) (or (open sK25) (= _let_0 sK25) (not (part_of sK25 _let_0)))))
(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open sK25) (= _let_0 sK25) (not (part_of sK25 _let_0)))))
(assert (let ((_let_0 (sum sK24 sK24))) (or (open sK26) (= _let_0 sK26) (not (part_of sK26 _let_0)))))
(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open sK26) (= _let_0 sK26) (not (part_of sK26 _let_0)))))
(assert (let ((_let_0 (sum sK24 sK24))) (or (open _let_0) (not (part_of _let_0 sK25)) (= sK25 _let_0))))
(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open _let_0) (not (part_of _let_0 sK25)) (= sK25 _let_0))))
(assert (let ((_let_0 (sum sK24 sK24))) (or (open _let_0) (not (part_of _let_0 sK26)) (= sK26 _let_0))))
(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open _let_0) (not (part_of _let_0 sK26)) (= sK26 _let_0))))
(assert (let ((_let_0 (sum sK24 sK24))) (let ((_let_1 (sK12 _let_0 sK25))) (or (= sK25 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK25)))))
(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (let ((_let_1 (sK12 _let_0 sK25))) (or (= sK25 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK25)))))
(assert (let ((_let_0 (sum sK24 sK24))) (let ((_let_1 (sK12 _let_0 sK26))) (or (= sK26 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK26)))))
(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (let ((_let_1 (sK12 _let_0 sK26))) (or (= sK26 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK26)))))
(assert (let ((_let_0 (sK19 sK24))) (or (not (incident_o sK25 sK24)) (not (start_point _let_0 sK24)) (ordered_by sK24 _let_0 sK25) (= _let_0 sK25))))
(assert (let ((_let_0 (sK19 iProver_c13))) (or (not (start_point _let_0 iProver_c13)) (not (incident_o sK25 iProver_c13)) (ordered_by iProver_c13 _let_0 sK25) (= _let_0 sK25))))
(assert (let ((_let_0 (sK19 sK24))) (or (not (incident_o sK26 sK24)) (not (start_point _let_0 sK24)) (ordered_by sK24 _let_0 sK26) (= _let_0 sK26))))
(assert (let ((_let_0 (sK19 iProver_c13))) (or (not (start_point _let_0 iProver_c13)) (not (incident_o sK26 iProver_c13)) (ordered_by iProver_c13 _let_0 sK26) (= _let_0 sK26))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (or (incident_o _let_0 sK26) (not (ordered_by sK26 _let_0 sK24)))))
(assert (or (not (ordered_by sK26 (sK21 sK25 sK26) sK24)) (incident_o sK24 sK26)))
(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 sK24)) (between_o sK26 _let_0 sK24 sK24))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 iProver_c13)) (between_o sK26 _let_0 sK24 iProver_c13))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 sK24)) (between_o sK26 sK24 sK24 _let_0))))
(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 iProver_c13)) (between_o sK26 iProver_c13 sK24 _let_0))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (or (incident_o _let_0 sK25) (not (ordered_by sK25 _let_0 sK24)))))
(assert (or (not (ordered_by sK25 (sK21 sK26 sK25) sK24)) (incident_o sK24 sK25)))
(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 sK24)) (between_o sK25 _let_0 sK24 sK24))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 iProver_c13)) (between_o sK25 _let_0 sK24 iProver_c13))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 sK24)) (between_o sK25 sK24 sK24 _let_0))))
(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 iProver_c13)) (between_o sK25 iProver_c13 sK24 _let_0))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24)))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2))))))
(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0)))))
(check-sat)