src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.certs
author haftmann
Thu, 24 Jul 2025 17:46:29 +0200
changeset 82902 99a720d3ed8f
parent 78676 a98e0a816d28
permissions -rw-r--r--
clarified code setup
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78676
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     1
35b253bd6d27f6991af73e29ed1030cb74b50ab2 11 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     2
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     3
(assume conjecture0 (not (! (= (! (- c$ b$) :named @p_2) a$) :named @p_1)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     4
(assume hypothesis1 (! (= c$ (+ a$ b$)) :named @p_6))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     5
(step t3 (cl (or @p_1 (! (not (! (<= @p_2 a$) :named @p_5)) :named @p_3) (! (not (! (<= a$ @p_2) :named @p_7)) :named @p_4))) :rule la_disequality)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     6
(step t4 (cl @p_1 @p_3 @p_4) :rule or :premises (t3))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     7
(step t5 (cl @p_3 @p_4) :rule resolution :premises (t4 conjecture0))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     8
(step t6 (cl @p_5 (! (not @p_6) :named @p_8)) :rule la_generic :args (1 (- 1)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
     9
(step t7 (cl @p_5) :rule resolution :premises (t6 hypothesis1))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    10
(step t8 (cl @p_4) :rule resolution :premises (t5 t7))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    11
(step t9 (cl @p_7 @p_8) :rule la_generic :args (1 1))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    12
(step t10 (cl) :rule resolution :premises (t9 hypothesis1 t8))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    13
882414839a017a484227974e42bc9854cb971d88 49 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    14
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    15
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    16
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    17
(let ((?x49 (* (- 1) a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    18
(let ((?x36 (* (- 1) b$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    19
(let ((?x50 (+ c$ ?x36 ?x49)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    20
(let (($x92 (= ?x50 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    21
(let (($x114 (not $x92)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    22
(let ((@x128 (rewrite (= (not true) false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    23
(let (($x55 (>= ?x50 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    24
(let (($x89 (not $x55)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    25
(let (($x51 (<= ?x50 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    26
(let (($x86 (not $x51)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    27
(let (($x101 (or $x92 $x86 $x89)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    28
(let (($x57 (and $x51 $x55)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    29
(let ((@x59 (monotonicity (rewrite (= (<= (+ c$ ?x36) a$) $x51)) (rewrite (= (<= a$ (+ c$ ?x36)) $x55)) (= (and (<= (+ c$ ?x36) a$) (<= a$ (+ c$ ?x36))) $x57))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    30
(let ((?x29 (- c$ b$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    31
(let (($x32 (<= a$ ?x29)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    32
(let (($x31 (<= ?x29 a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    33
(let (($x33 (and $x31 $x32)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    34
(let ((@x39 (rewrite (= ?x29 (+ c$ ?x36)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    35
(let ((@x48 (monotonicity (monotonicity @x39 (= $x31 (<= (+ c$ ?x36) a$))) (monotonicity @x39 (= $x32 (<= a$ (+ c$ ?x36)))) (= $x33 (and (<= (+ c$ ?x36) a$) (<= a$ (+ c$ ?x36)))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    36
(let ((@x64 (and-elim (mp (asserted $x33) (trans @x48 @x59 (= $x33 $x57)) $x57) $x55)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    37
(let ((@x132 (monotonicity (iff-true @x64 (= $x55 true)) (= $x89 (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    38
(let ((@x63 (and-elim (mp (asserted $x33) (trans @x48 @x59 (= $x33 $x57)) $x57) $x51)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    39
(let ((@x126 (monotonicity (iff-true @x63 (= $x51 true)) (= $x86 (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    40
(let ((@x137 (monotonicity (trans @x126 @x128 (= $x86 false)) (trans @x132 @x128 (= $x89 false)) (= $x101 (or $x92 false false)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    41
(let ((@x141 (trans @x137 (rewrite (= (or $x92 false false) $x92)) (= $x101 $x92))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    42
(let ((?x37 (+ c$ ?x36)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    43
(let (($x43 (<= a$ ?x37)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    44
(let (($x77 (not $x43)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    45
(let (($x40 (<= ?x37 a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    46
(let (($x74 (not $x40)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    47
(let (($x80 (or $x74 $x77)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    48
(let (($x71 (= ?x37 a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    49
(let (($x83 (or $x71 $x80)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    50
(let ((@x97 (monotonicity (monotonicity (rewrite (= $x40 $x51)) (= $x74 $x86)) (monotonicity (rewrite (= $x43 $x55)) (= $x77 $x89)) (= $x80 (or $x86 $x89)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    51
(let ((@x100 (monotonicity (rewrite (= $x71 $x92)) @x97 (= $x83 (or $x92 (or $x86 $x89))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    52
(let ((@x105 (trans @x100 (rewrite (= (or $x92 (or $x86 $x89)) $x101)) (= $x83 $x101))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    53
(let ((@x79 (monotonicity (monotonicity @x39 (= $x32 $x43)) (= (not $x32) $x77))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    54
(let ((@x76 (monotonicity (monotonicity @x39 (= $x31 $x40)) (= (not $x31) $x74))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    55
(let ((@x85 (monotonicity (monotonicity @x39 (= (= ?x29 a$) $x71)) (monotonicity @x76 @x79 (= (or (not $x31) (not $x32)) $x80)) (= (or (= ?x29 a$) (or (not $x31) (not $x32))) $x83))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    56
(let ((@x107 (trans @x85 @x105 (= (or (= ?x29 a$) (or (not $x31) (not $x32))) $x101))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    57
(let ((@x108 (mp (asserted (or (= ?x29 a$) (or (not $x31) (not $x32)))) @x107 $x101)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    58
(let ((@x146 (monotonicity (iff-true (mp @x108 @x141 $x92) (= $x92 true)) (= $x114 (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    59
(let ((@x113 (monotonicity (monotonicity @x39 (= (= ?x29 a$) $x71)) (= (not (= ?x29 a$)) (not $x71)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    60
(let ((@x118 (trans @x113 (monotonicity (rewrite (= $x71 $x92)) (= (not $x71) $x114)) (= (not (= ?x29 a$)) $x114))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    61
(mp (mp (asserted (not (= ?x29 a$))) @x118 $x114) (trans @x146 @x128 (= $x114 false)) false)))))))))))))))))))))))))))))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    62
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    63
f2541774823d4fd4ada0de04dcf1ccc81465be15 38 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    64
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    65
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    66
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    67
(let ((?x69 (* (- 1) a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    68
(let ((?x41 (* (- 1) b$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    69
(let ((?x70 (+ c$ ?x41 ?x69)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    70
(let (($x78 (>= ?x70 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    71
(let (($x80 (not $x78)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    72
(let (($x71 (<= ?x70 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    73
(let (($x74 (not $x71)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    74
(let (($x83 (= ?x70 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    75
(let (($x92 (or $x83 $x74 $x80)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    76
(let (($x97 (not $x92)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    77
(let (($x37 (or (= (- c$ b$) a$) (or (not (<= (- c$ b$) a$)) (not (<= a$ (- c$ b$)))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    78
(let (($x38 (not $x37)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    79
(let ((?x42 (+ c$ ?x41)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    80
(let (($x54 (<= a$ ?x42)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    81
(let (($x57 (not $x54)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    82
(let (($x48 (<= ?x42 a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    83
(let (($x51 (not $x48)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    84
(let (($x60 (or $x51 $x57)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    85
(let (($x45 (= ?x42 a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    86
(let (($x63 (or $x45 $x60)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    87
(let ((@x88 (monotonicity (monotonicity (rewrite (= $x48 $x71)) (= $x51 $x74)) (monotonicity (rewrite (= $x54 $x78)) (= $x57 $x80)) (= $x60 (or $x74 $x80)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    88
(let ((@x91 (monotonicity (rewrite (= $x45 $x83)) @x88 (= $x63 (or $x83 (or $x74 $x80))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    89
(let ((@x96 (trans @x91 (rewrite (= (or $x83 (or $x74 $x80)) $x92)) (= $x63 $x92))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    90
(let (($x61 (= (or (not (<= (- c$ b$) a$)) (not (<= a$ (- c$ b$)))) $x60)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    91
(let ((@x44 (rewrite (= (- c$ b$) ?x42))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    92
(let ((@x59 (monotonicity (monotonicity @x44 (= (<= a$ (- c$ b$)) $x54)) (= (not (<= a$ (- c$ b$))) $x57))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    93
(let ((@x53 (monotonicity (monotonicity @x44 (= (<= (- c$ b$) a$) $x48)) (= (not (<= (- c$ b$) a$)) $x51))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    94
(let ((@x65 (monotonicity (monotonicity @x44 (= (= (- c$ b$) a$) $x45)) (monotonicity @x53 @x59 $x61) (= $x37 $x63))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    95
(let ((@x101 (trans (monotonicity @x65 (= $x38 (not $x63))) (monotonicity @x96 (= (not $x63) $x97)) (= $x38 $x97))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    96
(let ((@x102 (mp (asserted $x38) @x101 $x97)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    97
(let ((@x106 (not-or-elim @x102 $x78)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    98
(let ((@x104 (not-or-elim @x102 (not $x83))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
    99
(let ((@x105 (not-or-elim @x102 $x71)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   100
(unit-resolution ((_ th-lemma arith triangle-eq) $x92) @x105 @x104 @x106 false))))))))))))))))))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   101
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   102
38c94308bfb0b4491339a6c117e29fba807f290a 27 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   103
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   104
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   105
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   106
(let ((?x41 (* (- 1) c$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   107
(let ((?x42 (+ a$ ?x41 b$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   108
(let (($x43 (<= ?x42 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   109
(let (($x55 (>= ?x42 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   110
(let (($x69 (and $x55 $x43)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   111
(let (($x72 (not $x69)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   112
(let ((@x40 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= a$ (- c$ b$)) (<= a$ (+ c$ (* (- 1) b$)))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   113
(let ((@x47 (trans @x40 (rewrite (= (<= a$ (+ c$ (* (- 1) b$))) $x43)) (= (<= a$ (- c$ b$)) $x43))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   114
(let ((@x79 (iff-true (mp (asserted (<= a$ (- c$ b$))) @x47 $x43) (= $x43 true))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   115
(let ((@x53 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= (- c$ b$) a$) (<= (+ c$ (* (- 1) b$)) a$)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   116
(let ((@x58 (trans @x53 (rewrite (= (<= (+ c$ (* (- 1) b$)) a$) $x55)) (= (<= (- c$ b$) a$) $x55))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   117
(let ((@x81 (iff-true (mp (asserted (<= (- c$ b$) a$)) @x58 $x55) (= $x55 true))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   118
(let ((@x88 (trans (monotonicity @x81 @x79 (= $x69 (and true true))) (rewrite (= (and true true) true)) (= $x69 true))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   119
(let ((@x95 (trans (monotonicity @x88 (= $x72 (not true))) (rewrite (= (not true) false)) (= $x72 false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   120
(let (($x61 (not (and (<= (- c$ b$) a$) (<= a$ (- c$ b$))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   121
(let ((?x35 (+ c$ (* (- 1) b$))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   122
(let (($x38 (<= a$ ?x35)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   123
(let (($x51 (<= ?x35 a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   124
(let (($x63 (and $x51 $x38)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   125
(let ((@x71 (monotonicity (rewrite (= $x51 $x55)) (rewrite (= $x38 $x43)) (= $x63 $x69))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   126
(let ((@x65 (monotonicity @x53 @x40 (= (and (<= (- c$ b$) a$) (<= a$ (- c$ b$))) $x63))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   127
(let ((@x76 (trans (monotonicity @x65 (= $x61 (not $x63))) (monotonicity @x71 (= (not $x63) $x72)) (= $x61 $x72))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   128
(mp (mp (asserted $x61) @x76 $x72) @x95 false)))))))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   129
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   130
d40f5f06cb71bf04976dfbd768e98729d8a02410 29 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   131
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   132
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   133
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   134
(let ((?x36 (* (- 1) c$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   135
(let ((?x37 (+ a$ b$ ?x36)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   136
(let (($x56 (<= ?x37 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   137
(let (($x38 (= ?x37 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   138
(let ((@x41 (mp (asserted (= (+ a$ b$) c$)) (rewrite (= (= (+ a$ b$) c$) $x38)) $x38)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   139
(let ((@x85 (monotonicity (iff-true @x41 (= $x38 true)) (= (not $x38) (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   140
(let ((@x89 (trans @x85 (rewrite (= (not true) false)) (= (not $x38) false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   141
(let ((@x96 (trans (monotonicity @x89 (= (or $x56 (not $x38)) (or $x56 false))) (rewrite (= (or $x56 false) $x56)) (= (or $x56 (not $x38)) $x56))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   142
(let (($x61 (not $x38)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   143
(let (($x64 (or $x56 $x61)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   144
(let (($x43 (not (= c$ (+ a$ b$)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   145
(let (($x34 (<= a$ (- c$ b$))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   146
(let (($x44 (or $x34 $x43)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   147
(let ((@x63 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x38)) (= $x43 $x61))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   148
(let ((@x66 (monotonicity (rewrite (= (<= a$ (+ (* (- 1) b$) c$)) $x56)) @x63 (= (or (<= a$ (+ (* (- 1) b$) c$)) $x43) $x64))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   149
(let ((@x52 (monotonicity (rewrite (= (- c$ b$) (+ (* (- 1) b$) c$))) (= $x34 (<= a$ (+ (* (- 1) b$) c$))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   150
(let ((@x55 (monotonicity @x52 (= $x44 (or (<= a$ (+ (* (- 1) b$) c$)) $x43)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   151
(let ((@x97 (mp (mp (asserted $x44) (trans @x55 @x66 (= $x44 $x64)) $x64) @x96 $x56)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   152
(let ((@x101 (monotonicity (iff-true @x97 (= $x56 true)) (= (not $x56) (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   153
(let ((@x103 (trans @x101 (rewrite (= (not true) false)) (= (not $x56) false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   154
(let (($x75 (not $x56)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   155
(let ((@x77 (monotonicity (rewrite (= (<= a$ (+ (* (- 1) b$) c$)) $x56)) (= (not (<= a$ (+ (* (- 1) b$) c$))) $x75))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   156
(let ((@x74 (monotonicity @x52 (= (not $x34) (not (<= a$ (+ (* (- 1) b$) c$)))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   157
(let ((@x80 (mp (asserted (not $x34)) (trans @x74 @x77 (= (not $x34) $x75)) $x75)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   158
(mp @x80 @x103 false)))))))))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   159
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   160
589302410c98bf9494c2b8bba0d198d5d6fb8f30 22 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   161
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   162
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   163
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   164
(let (($x58 (= (+ a$ (* (- 1) c$) b$) 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   165
(let (($x66 (not (or (<= (+ a$ (* (- 1) c$) b$) 0) (not $x58)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   166
(let (($x36 (not (or (<= a$ (- c$ b$)) (not (= c$ (+ a$ b$)))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   167
(let (($x34 (not (= c$ (+ a$ b$)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   168
(let (($x43 (<= a$ (+ c$ (* (- 1) b$)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   169
(let (($x46 (or $x43 $x34)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   170
(let ((@x62 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x58)) (= $x34 (not $x58)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   171
(let ((@x65 (monotonicity (rewrite (= $x43 (<= (+ a$ (* (- 1) c$) b$) 0))) @x62 (= $x46 (or (<= (+ a$ (* (- 1) c$) b$) 0) (not $x58))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   172
(let ((@x45 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= a$ (- c$ b$)) $x43))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   173
(let ((@x51 (monotonicity (monotonicity @x45 (= (or (<= a$ (- c$ b$)) $x34) $x46)) (= $x36 (not $x46)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   174
(let ((@x70 (trans @x51 (monotonicity @x65 (= (not $x46) $x66)) (= $x36 $x66))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   175
(let ((@x75 (monotonicity (not-or-elim (mp (asserted $x36) @x70 $x66) $x58) (= (<= (+ a$ (* (- 1) c$) b$) 0) (<= 0 0)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   176
(let ((@x81 (trans @x75 (rewrite (= (<= 0 0) true)) (= (<= (+ a$ (* (- 1) c$) b$) 0) true))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   177
(let ((@x84 (monotonicity @x81 (= (not (<= (+ a$ (* (- 1) c$) b$) 0)) (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   178
(let ((@x88 (trans @x84 (rewrite (= (not true) false)) (= (not (<= (+ a$ (* (- 1) c$) b$) 0)) false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   179
(let (($x54 (<= (+ a$ (* (- 1) c$) b$) 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   180
(let (($x72 (not $x54)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   181
(mp (not-or-elim (mp (asserted $x36) @x70 $x66) $x72) @x88 false))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   182
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   183
a19eb65c252ea63e4442473afd12fc3c9abc7d26 29 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   184
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   185
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   186
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   187
(let ((?x36 (* (- 1) c$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   188
(let ((?x37 (+ a$ b$ ?x36)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   189
(let (($x57 (>= ?x37 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   190
(let (($x38 (= ?x37 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   191
(let ((@x41 (mp (asserted (= (+ a$ b$) c$)) (rewrite (= (= (+ a$ b$) c$) $x38)) $x38)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   192
(let ((@x85 (monotonicity (iff-true @x41 (= $x38 true)) (= (not $x38) (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   193
(let ((@x89 (trans @x85 (rewrite (= (not true) false)) (= (not $x38) false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   194
(let ((@x96 (trans (monotonicity @x89 (= (or $x57 (not $x38)) (or $x57 false))) (rewrite (= (or $x57 false) $x57)) (= (or $x57 (not $x38)) $x57))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   195
(let (($x61 (not $x38)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   196
(let (($x64 (or $x57 $x61)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   197
(let (($x43 (not (= c$ (+ a$ b$)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   198
(let (($x34 (<= (- c$ b$) a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   199
(let (($x44 (or $x34 $x43)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   200
(let ((@x63 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x38)) (= $x43 $x61))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   201
(let ((@x66 (monotonicity (rewrite (= (<= (+ (* (- 1) b$) c$) a$) $x57)) @x63 (= (or (<= (+ (* (- 1) b$) c$) a$) $x43) $x64))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   202
(let ((@x52 (monotonicity (rewrite (= (- c$ b$) (+ (* (- 1) b$) c$))) (= $x34 (<= (+ (* (- 1) b$) c$) a$)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   203
(let ((@x55 (monotonicity @x52 (= $x44 (or (<= (+ (* (- 1) b$) c$) a$) $x43)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   204
(let ((@x97 (mp (mp (asserted $x44) (trans @x55 @x66 (= $x44 $x64)) $x64) @x96 $x57)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   205
(let ((@x101 (monotonicity (iff-true @x97 (= $x57 true)) (= (not $x57) (not true)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   206
(let ((@x103 (trans @x101 (rewrite (= (not true) false)) (= (not $x57) false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   207
(let (($x75 (not $x57)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   208
(let ((@x77 (monotonicity (rewrite (= (<= (+ (* (- 1) b$) c$) a$) $x57)) (= (not (<= (+ (* (- 1) b$) c$) a$)) $x75))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   209
(let ((@x74 (monotonicity @x52 (= (not $x34) (not (<= (+ (* (- 1) b$) c$) a$))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   210
(let ((@x80 (mp (asserted (not $x34)) (trans @x74 @x77 (= (not $x34) $x75)) $x75)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   211
(mp @x80 @x103 false)))))))))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   212
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   213
4935c5af5b588fd6e477bea2bed6285c3e17b0c6 23 0
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   214
unsat
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   215
((set-logic AUFLIA)
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   216
(proof
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   217
(let (($x63 (<= (+ c$ (* (- 1) b$) (* (- 1) a$)) 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   218
(let (($x81 (not $x63)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   219
(let (($x66 (= (+ c$ (* (- 1) b$) (* (- 1) a$)) 0)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   220
(let (($x75 (not (or $x63 (not $x66)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   221
(let (($x36 (not (or (<= (- c$ b$) a$) (not (= c$ (+ a$ b$)))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   222
(let (($x49 (= c$ (+ b$ a$))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   223
(let (($x52 (not $x49)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   224
(let (($x43 (<= (+ c$ (* (- 1) b$)) a$)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   225
(let (($x55 (or $x43 $x52)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   226
(let ((@x74 (monotonicity (rewrite (= $x43 $x63)) (monotonicity (rewrite (= $x49 $x66)) (= $x52 (not $x66))) (= $x55 (or $x63 (not $x66))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   227
(let (($x56 (= (or (<= (- c$ b$) a$) (not (= c$ (+ a$ b$)))) $x55)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   228
(let ((@x51 (monotonicity (rewrite (= (+ a$ b$) (+ b$ a$))) (= (= c$ (+ a$ b$)) $x49))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   229
(let ((@x45 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= (- c$ b$) a$) $x43))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   230
(let ((@x57 (monotonicity @x45 (monotonicity @x51 (= (not (= c$ (+ a$ b$))) $x52)) $x56)))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   231
(let ((@x79 (trans (monotonicity @x57 (= $x36 (not $x55))) (monotonicity @x74 (= (not $x55) $x75)) (= $x36 $x75))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   232
(let ((@x84 (monotonicity (not-or-elim (mp (asserted $x36) @x79 $x75) $x66) (= $x63 (<= 0 0)))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   233
(let ((@x90 (trans @x84 (rewrite (= (<= 0 0) true)) (= $x63 true))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   234
(let ((@x97 (trans (monotonicity @x90 (= $x81 (not true))) (rewrite (= (not true) false)) (= $x81 false))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   235
(mp (not-or-elim (mp (asserted $x36) @x79 $x75) $x81) @x97 false)))))))))))))))))))))
a98e0a816d28 added first proof reconstruction test for Sledgehammer
desharna
parents:
diff changeset
   236