File ‹Sledgehammer_Isar_Proofs.certs›

1af9d054abf82d7efd8f23f74121934e0afad902 13 0
unsat
(
(assume conjecture0 (not c$))
(assume a1 (=> b$ c$))
(assume a2 (=> a$ c$))
(assume a3 (or a$ b$))
(step t5 (cl (! (not b$) :named @p_1) c$) :rule implies :premises (a1))
(step t6 (cl @p_1) :rule resolution :premises (t5 conjecture0))
(step t7 (cl (! (not a$) :named @p_2) c$) :rule implies :premises (a2))
(step t8 (cl @p_2) :rule resolution :premises (t7 conjecture0))
(step t9 (cl a$ b$) :rule or :premises (a3))
(step t10 (cl) :rule resolution :premises (t9 t6 t8))
)
1eda9081935e160e22123b1bbe1aad97d193c0f0 7 0
unsat
(
conjecture0
a1
a2
a3
)
77ee752712f4c8fe3f5a682f2c46b513d902ca91 17 0
unsat
((set-logic AUFLIA)
(proof
(let (($x33 (not b$)))
(let ((@x52 (monotonicity (iff-false (asserted (not c$)) (= c$ false)) (= (or $x33 c$) (or $x33 false)))))
(let ((@x56 (trans @x52 (rewrite (= (or $x33 false) $x33)) (= (or $x33 c$) $x33))))
(let (($x34 (or $x33 c$)))
(let ((@x39 (mp (asserted (=> b$ c$)) (rewrite (= (=> b$ c$) $x34)) $x34)))
(let (($x41 (not a$)))
(let ((@x62 (monotonicity (iff-false (asserted (not c$)) (= c$ false)) (= (or $x41 c$) (or $x41 false)))))
(let ((@x66 (trans @x62 (rewrite (= (or $x41 false) $x41)) (= (or $x41 c$) $x41))))
(let (($x42 (or $x41 c$)))
(let ((@x47 (mp (asserted (=> a$ c$)) (rewrite (= (=> a$ c$) $x42)) $x42)))
(let ((@x72 (monotonicity (iff-false (mp @x47 @x66 $x41) (= a$ false)) (iff-false (mp @x39 @x56 $x33) (= b$ false)) (= (or a$ b$) (or false false)))))
(let ((@x76 (trans @x72 (rewrite (= (or false false) false)) (= (or a$ b$) false))))
(mp (asserted (or a$ b$)) @x76 false)))))))))))))))

8984d5bf3201c516127d624643be532f1c323b6b 4 0
unsat
(
conjecture0
)
7e2c403a5208b46b5873bfeaa0dd8e2644b7159a 17 0
unsat
(
(assume conjecture0 (! (not (! (= (! (ite p$ a$ b$) :named @p_2) (ite (not p$) b$ a$)) :named @p_1)) :named @p_4))
(step t2 (cl @p_1) :rule ite_simplify)
(step t3 (cl (= @p_1 (! (= @p_2 @p_2) :named @p_3))) :rule cong :premises (t2))
(step t4 (cl (= @p_3 true)) :rule eq_simplify)
(step t5 (cl (= @p_1 true)) :rule trans :premises (t3 t4))
(step t6 (cl (= @p_4 (! (not true) :named @p_5))) :rule cong :premises (t5))
(step t7 (cl (= @p_5 false)) :rule not_simplify)
(step t8 (cl (! (= @p_4 false) :named @p_6)) :rule trans :premises (t6 t7))
(step t9 (cl (! (not @p_6) :named @p_8) (! (not @p_4) :named @p_7) false) :rule equiv_pos2)
(step t10 (cl (not @p_7) @p_1) :rule not_not)
(step t11 (cl @p_8 @p_1 false) :rule th_resolution :premises (t10 t9))
(step t12 (cl false) :rule th_resolution :premises (conjecture0 t8 t11))
(step t13 (cl (not false)) :rule false)
(step t14 (cl) :rule resolution :premises (t12 t13))
)
0d8670d2c812e7ed70b73dd858e4c41479236d6d 12 0
unsat
((set-logic AUFLIA)
(proof
(let (($x31 (not p$)))
(let ((?x32 (ite $x31 b$ a$)))
(let ((?x30 (ite p$ a$ b$)))
(let (($x33 (= ?x30 ?x32)))
(let (($x34 (not $x33)))
(let ((@x44 (trans (monotonicity (rewrite (= ?x32 ?x30)) (= $x33 (= ?x30 ?x30))) (rewrite (= (= ?x30 ?x30) true)) (= $x33 true))))
(let ((@x51 (trans (monotonicity @x44 (= $x34 (not true))) (rewrite (= (not true) false)) (= $x34 false))))
(mp (asserted $x34) @x51 false))))))))))