```
``````
unsat
((set-logic <null>)
(proof
(let ((@x41 (monotonicity (rewrite (= (<= 2 a) (>= a 2))) (= (not (<= 2 a)) (not (>= a 2))))))
(let (($x19 (<= 2 a)))
(let (($x20 (not $x19)))
(let ((@x26 (monotonicity (rewrite (= $x19 $x19)) (= $x20 $x20))))
(let ((@x27 (trans (rewrite (= (< a 2) $x20)) @x26 (= (< a 2) $x20))))
(let (($x7 (< a 2)))
(let ((@x29 (mp (mp (|and-elim| (asserted (and (> a 3) $x7)) $x7) @x27 $x20) @x26 $x20)))
(let ((@x42 (mp (mp (mp @x29 (|rewrite*| (= $x20 $x20)) $x20) @x26 $x20) @x41 (not (>= a 2)))))
(let (($x39 (>= a 2)))
(let (($x15 (not (<= a 3))))
(let ((@x18 (mp (|and-elim| (asserted (and (> a 3) $x7)) (> a 3)) (rewrite (= (> a 3) $x15)) $x15)))
(let ((@x64 (|unit-resolution| ((_ |th-lemma| arith farkas 1 1) (or $x39 (<= a 3))) (mp @x18 (|rewrite*| (= $x15 $x15)) $x15) $x39)))
(|unit-resolution| @x64 @x42 false)))))))))))))))
```

Looking good, right? Well, hardly.Even with nicer formatting, line breaks, etc. the proof is not quite readable. Now, it looks like people have actually managed to work with these proofs and I'm quite curious about how they accomplished that. There is a description of all the symbols used in the proof, but what I'm lacking is some kind of command line parameter which simply feeds the proof back into Z3.

If I ever find one (or build one), I'll write down here.

## Keine Kommentare:

## Kommentar veröffentlichen