diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/GEO123+1.minimized.smt2 | 397 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 |
2 files changed, 398 insertions, 0 deletions
diff --git a/test/regress/regress0/GEO123+1.minimized.smt2 b/test/regress/regress0/GEO123+1.minimized.smt2 new file mode 100644 index 000000000..8cc1fa7fd --- /dev/null +++ b/test/regress/regress0/GEO123+1.minimized.smt2 @@ -0,0 +1,397 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +; +; 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) + diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index fec081ca8..4c14de996 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -115,6 +115,7 @@ TPTP_TESTS = \ # Regression tests derived from bug reports BUG_TESTS = \ + GEO123+1.minimized.smt2 \ smt2output.smt2 \ bug32.cvc \ bug49.smt \ |