378 (let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31))))) |
378 (let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31))))) |
379 (let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true))))) |
379 (let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true))))) |
380 (let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false)))) |
380 (let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false)))) |
381 (mp (asserted (not $x32)) @x53 false)))))))))) |
381 (mp (asserted (not $x32)) @x53 false)))))))))) |
382 |
382 |
|
383 9f7a96d88c6326ad836384c37d13934828ff726d 8 0 |
|
384 unsat |
|
385 ((set-logic <null>) |
|
386 (proof |
|
387 (let ((@x38 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4)))))) |
|
388 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true)))) |
|
389 (let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false)))) |
|
390 (mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false)))))) |
|
391 |
|
392 6cad4ca9b92628993328e0c9cd5982fe4690567b 7 0 |
|
393 unsat |
|
394 ((set-logic <null>) |
|
395 (proof |
|
396 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true))))) |
|
397 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false)))) |
|
398 (mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false))))) |
|
399 |
|
400 55b7bec34258b475381a754439390616488c924c 7 0 |
|
401 unsat |
|
402 ((set-logic <null>) |
|
403 (proof |
|
404 (let ((@x38 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true))))) |
|
405 (let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false)))) |
|
406 (mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x42 false))))) |
|
407 |
|
408 fa462c1327b4231dc12d6f379b9bb280ea17bfd3 9 0 |
|
409 unsat |
|
410 ((set-logic <null>) |
|
411 (proof |
|
412 (let ((@x38 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5)))))) |
|
413 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true)))) |
|
414 (let ((@x45 (monotonicity @x42 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true))))) |
|
415 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false)))) |
|
416 (mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x49 false))))))) |
|
417 |
|
418 bf6c2eb2daf9373dd063355969e25afc57fc44fe 9 0 |
|
419 unsat |
|
420 ((set-logic <null>) |
|
421 (proof |
|
422 (let ((@x38 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8)))))) |
|
423 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true)))) |
|
424 (let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true))))) |
|
425 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false)))) |
|
426 (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false))))))) |
|
427 |
|
428 21dcbc62e4a0d275653bc7c57a948d4bf6975168 9 0 |
|
429 unsat |
|
430 ((set-logic <null>) |
|
431 (proof |
|
432 (let ((@x43 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8)))))) |
|
433 (let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true)))) |
|
434 (let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true))))) |
|
435 (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false)))) |
|
436 (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false))))))) |
|
437 |
|
438 6dd961e81bf75734a230f5a110b28edf98e90aaf 7 0 |
|
439 unsat |
|
440 ((set-logic <null>) |
|
441 (proof |
|
442 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) |
|
443 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) |
|
444 (mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false))))) |
|
445 |
|
446 10d0fe43a5dca47373c59ffadf5d4a9049a8df88 11 0 |
|
447 unsat |
|
448 ((set-logic <null>) |
|
449 (proof |
|
450 (let ((@x42 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7)))))) |
|
451 (let ((@x47 (trans @x42 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7))))) |
|
452 (let ((@x52 (monotonicity @x47 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7)))))) |
|
453 (let ((@x56 (trans @x52 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true)))) |
|
454 (let ((@x59 (monotonicity @x56 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true))))) |
|
455 (let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false)))) |
|
456 (mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false))))))))) |
|
457 |
|
458 de1bc26329091943d56ccf83cf9662c0b2001c97 19 0 |
|
459 unsat |
|
460 ((set-logic <null>) |
|
461 (proof |
|
462 (let ((?x35 (bvadd b$ c$))) |
|
463 (let ((?x36 (bvadd ?x35 a$))) |
|
464 (let ((?x30 (bvmul (_ bv2 32) b$))) |
|
465 (let ((?x31 (bvadd a$ ?x30))) |
|
466 (let ((?x33 (bvadd ?x31 c$))) |
|
467 (let ((?x34 (bvsub ?x33 b$))) |
|
468 (let (($x37 (= ?x34 ?x36))) |
|
469 (let (($x38 (not $x37))) |
|
470 (let ((@x58 (rewrite (= (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)) true)))) |
|
471 (let ((@x48 (rewrite (= (bvsub (bvadd a$ ?x30 c$) b$) (bvadd a$ b$ c$))))) |
|
472 (let ((@x46 (monotonicity (rewrite (= ?x33 (bvadd a$ ?x30 c$))) (= ?x34 (bvsub (bvadd a$ ?x30 c$) b$))))) |
|
473 (let ((@x56 (monotonicity (trans @x46 @x48 (= ?x34 (bvadd a$ b$ c$))) (rewrite (= ?x36 (bvadd a$ b$ c$))) (= $x37 (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)))))) |
|
474 (let ((@x63 (monotonicity (trans @x56 @x58 (= $x37 true)) (= $x38 (not true))))) |
|
475 (let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false)))) |
|
476 (mp (asserted $x38) @x67 false))))))))))))))))) |
|
477 |
|
478 821acdf5acf235899fac29bcb5ad69c40cffe88f 18 0 |
|
479 unsat |
|
480 ((set-logic <null>) |
|
481 (proof |
|
482 (let ((?x31 (bvmul (_ bv4 4) x$))) |
|
483 (let (($x32 (= ?x31 (_ bv4 4)))) |
|
484 (let (($x43 (= (_ bv5 4) x$))) |
|
485 (let (($x56 (not (or (not $x43) (= (_ bv4 4) ?x31))))) |
|
486 (let ((@x48 (monotonicity (rewrite (= (= x$ (_ bv5 4)) $x43)) (= (not (= x$ (_ bv5 4))) (not $x43))))) |
|
487 (let ((@x55 (monotonicity @x48 (rewrite (= $x32 (= (_ bv4 4) ?x31))) (= (or (not (= x$ (_ bv5 4))) $x32) (or (not $x43) (= (_ bv4 4) ?x31)))))) |
|
488 (let (($x34 (not (=> (= x$ (_ bv5 4)) $x32)))) |
|
489 (let ((@x39 (rewrite (= (=> (= x$ (_ bv5 4)) $x32) (or (not (= x$ (_ bv5 4))) $x32))))) |
|
490 (let ((@x60 (trans (monotonicity @x39 (= $x34 (not (or (not (= x$ (_ bv5 4))) $x32)))) (monotonicity @x55 (= (not (or (not (= x$ (_ bv5 4))) $x32)) $x56)) (= $x34 $x56)))) |
|
491 (let ((@x67 (monotonicity (not-or-elim (mp (asserted $x34) @x60 $x56) $x43) (= ?x31 (bvmul (_ bv4 4) (_ bv5 4)))))) |
|
492 (let ((@x73 (monotonicity (trans @x67 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x32) (= (= (_ bv4 4) ?x31) (= (_ bv4 4) (_ bv4 4)))))) |
|
493 (let ((@x77 (trans @x73 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x31) true)))) |
|
494 (let ((@x84 (trans (monotonicity @x77 (= (not (= (_ bv4 4) ?x31)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x31)) false)))) |
|
495 (mp (not-or-elim (mp (asserted $x34) @x60 $x56) (not (= (_ bv4 4) ?x31))) @x84 false)))))))))))))))) |
|
496 |
|
497 fb4d74278af64850ed8084451a8ff7a7075dbdfe 9 0 |
|
498 unsat |
|
499 ((set-logic <null>) |
|
500 (proof |
|
501 (let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32)))))) |
|
502 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true)))) |
|
503 (let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true))))) |
|
504 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false)))) |
|
505 (mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false))))))) |
|
506 |
|
507 5a9d6d65605763b3b0286a0d4717a93a4da85a34 9 0 |
|
508 unsat |
|
509 ((set-logic <null>) |
|
510 (proof |
|
511 (let ((@x37 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8)))))) |
|
512 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true)))) |
|
513 (let ((@x44 (monotonicity @x41 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true))))) |
|
514 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false)))) |
|
515 (mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false))))))) |
|
516 |
|
517 71f993d99975ef37af8d8478a6f1c26548b6f4a7 9 0 |
|
518 unsat |
|
519 ((set-logic <null>) |
|
520 (proof |
|
521 (let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8)))))) |
|
522 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) |
|
523 (let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) |
|
524 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) |
|
525 (mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false))))))) |
|
526 |
|
527 353b2591bd8c22d0df29b19faf56739aac7b9b6d 8 0 |
|
528 unsat |
|
529 ((set-logic <null>) |
|
530 (proof |
|
531 (let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) |
|
532 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) |
|
533 (let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false)))) |
|
534 (mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false)))))) |
|
535 |
|
536 f40271ef9e5c8b600036568090a9c30a30fba3c1 9 0 |
|
537 unsat |
|
538 ((set-logic <null>) |
|
539 (proof |
|
540 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) |
|
541 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) |
|
542 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) |
|
543 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) |
|
544 (mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false))))))) |
|
545 |
|
546 98fd1bf6fea1dce9107b6a84cfa810d8ae0827ad 9 0 |
|
547 unsat |
|
548 ((set-logic <null>) |
|
549 (proof |
|
550 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) |
|
551 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) |
|
552 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) |
|
553 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false)))) |
|
554 (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false))))))) |
|
555 |
|
556 f5796d75c7b1d8ea9a2c70c40ab57315660fbcf3 8 0 |
|
557 unsat |
|
558 ((set-logic <null>) |
|
559 (proof |
|
560 (let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2)))))) |
|
561 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true)))) |
|
562 (let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false)))) |
|
563 (mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false)))))) |
|
564 |
|
565 44630a6139544aa8cc936f2dcdd464d5967b2876 9 0 |
|
566 unsat |
|
567 ((set-logic <null>) |
|
568 (proof |
|
569 (let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10)))))) |
|
570 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true)))) |
|
571 (let ((@x43 (monotonicity @x40 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true))))) |
|
572 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false)))) |
|
573 (mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false))))))) |
|
574 |
|
575 2b91c33c03a89b80ac6fb984f384bd9814c2b51d 9 0 |
|
576 unsat |
|
577 ((set-logic <null>) |
|
578 (proof |
|
579 (let ((@x36 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6)))))) |
|
580 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true)))) |
|
581 (let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true))))) |
|
582 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false)))) |
|
583 (mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false))))))) |
|
584 |
|
585 80e93d77c56b62b509cae750a834ba3c2a6545e3 9 0 |
|
586 unsat |
|
587 ((set-logic <null>) |
|
588 (proof |
|
589 (let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8)))))) |
|
590 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true)))) |
|
591 (let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true))))) |
|
592 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false)))) |
|
593 (mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false))))))) |
|
594 |
|
595 08e3a62c0a330f1ab742b05e694f723668925d10 9 0 |
|
596 unsat |
|
597 ((set-logic <null>) |
|
598 (proof |
|
599 (let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8)))))) |
|
600 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true)))) |
|
601 (let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true))))) |
|
602 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false)))) |
|
603 (mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false))))))) |
|
604 |
|
605 1b01af1c33961b4a329d46a526471313f71130ca 9 0 |
|
606 unsat |
|
607 ((set-logic <null>) |
|
608 (proof |
|
609 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4)))))) |
|
610 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true)))) |
|
611 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true))))) |
|
612 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false)))) |
|
613 (mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false))))))) |
|
614 |
|
615 d1e9761fb935892f82a21268d39aac76f75ee282 9 0 |
|
616 unsat |
|
617 ((set-logic <null>) |
|
618 (proof |
|
619 (let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8)))))) |
|
620 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true)))) |
|
621 (let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true))))) |
|
622 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false)))) |
|
623 (mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false))))))) |
|
624 |
|
625 a14e30a88e731b5e605d4726dbb1f583497ab894 9 0 |
|
626 unsat |
|
627 ((set-logic <null>) |
|
628 (proof |
|
629 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4)))))) |
|
630 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true)))) |
|
631 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true))))) |
|
632 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false)))) |
|
633 (mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false))))))) |
|
634 |
|
635 08dd0af4f9cea470363f78957650260a900928c8 17 0 |
|
636 unsat |
|
637 ((set-logic <null>) |
|
638 (proof |
|
639 (let ((?x31 (bvand x$ (_ bv255 16)))) |
|
640 (let ((?x29 (bvand x$ (_ bv65280 16)))) |
|
641 (let ((?x32 (bvor ?x29 ?x31))) |
|
642 (let (($x33 (= ?x32 x$))) |
|
643 (let (($x34 (not $x33))) |
|
644 (let ((@x59 (symm (commutativity (= (= x$ ?x32) $x33)) (= $x33 (= x$ ?x32))))) |
|
645 (let ((@x35 (asserted $x34))) |
|
646 (let ((@x63 (mp @x35 (monotonicity @x59 (= $x34 (not (= x$ ?x32)))) (not (= x$ ?x32))))) |
|
647 (let (($x52 (= x$ ?x32))) |
|
648 (let ((@x26 (true-axiom true))) |
|
649 (let (($x53 (or $x52 false false false false false false false false false false false false false false false false))) |
|
650 (let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52))) |
|
651 (unit-resolution @x55 @x63 false))))))))))))))) |
|
652 |
|
653 cffe711faa89f3f62e8e8e58173aaeb3cedc5d63 51 0 |
|
654 unsat |
|
655 ((set-logic <null>) |
|
656 (proof |
|
657 (let ((?x31 (bvand w$ (_ bv255 16)))) |
|
658 (let (($x32 (= ?x31 w$))) |
|
659 (let (($x64 (not $x32))) |
|
660 (let ((@x318 (symm (commutativity (= (= w$ ?x31) $x32)) (= $x32 (= w$ ?x31))))) |
|
661 (let (($x57 (not (or (bvule (_ bv256 16) w$) $x32)))) |
|
662 (let ((@x49 (monotonicity (rewrite (= (bvult w$ (_ bv256 16)) (not (bvule (_ bv256 16) w$)))) (= (not (bvult w$ (_ bv256 16))) (not (not (bvule (_ bv256 16) w$))))))) |
|
663 (let ((@x53 (trans @x49 (rewrite (= (not (not (bvule (_ bv256 16) w$))) (bvule (_ bv256 16) w$))) (= (not (bvult w$ (_ bv256 16))) (bvule (_ bv256 16) w$))))) |
|
664 (let ((@x56 (monotonicity @x53 (= (or (not (bvult w$ (_ bv256 16))) $x32) (or (bvule (_ bv256 16) w$) $x32))))) |
|
665 (let ((@x59 (monotonicity @x56 (= (not (or (not (bvult w$ (_ bv256 16))) $x32)) $x57)))) |
|
666 (let (($x34 (not (=> (bvult w$ (_ bv256 16)) $x32)))) |
|
667 (let ((@x39 (rewrite (= (=> (bvult w$ (_ bv256 16)) $x32) (or (not (bvult w$ (_ bv256 16))) $x32))))) |
|
668 (let ((@x42 (monotonicity @x39 (= $x34 (not (or (not (bvult w$ (_ bv256 16))) $x32)))))) |
|
669 (let ((@x65 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x64))) |
|
670 (let ((@x322 (mp @x65 (monotonicity @x318 (= $x64 (not (= w$ ?x31)))) (not (= w$ ?x31))))) |
|
671 (let (($x300 (= w$ ?x31))) |
|
672 (let (($x81 (= ((_ extract 15 15) w$) (_ bv1 1)))) |
|
673 (let (($x264 (not $x81))) |
|
674 (let (($x74 (= ((_ extract 8 8) w$) (_ bv1 1)))) |
|
675 (let (($x75 (= ((_ extract 9 9) w$) (_ bv1 1)))) |
|
676 (let (($x82 (and $x75 $x74))) |
|
677 (let (($x83 (or $x75 $x74 $x82))) |
|
678 (let (($x76 (= ((_ extract 10 10) w$) (_ bv1 1)))) |
|
679 (let (($x84 (and $x76 $x83))) |
|
680 (let (($x85 (or $x76 $x75 $x74 $x82 $x84))) |
|
681 (let (($x77 (= ((_ extract 11 11) w$) (_ bv1 1)))) |
|
682 (let (($x86 (and $x77 $x85))) |
|
683 (let (($x87 (or $x77 $x76 $x75 $x74 $x82 $x84 $x86))) |
|
684 (let (($x78 (= ((_ extract 12 12) w$) (_ bv1 1)))) |
|
685 (let (($x88 (and $x78 $x87))) |
|
686 (let (($x89 (or $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88))) |
|
687 (let (($x79 (= ((_ extract 13 13) w$) (_ bv1 1)))) |
|
688 (let (($x90 (and $x79 $x89))) |
|
689 (let (($x91 (or $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90))) |
|
690 (let (($x80 (= ((_ extract 14 14) w$) (_ bv1 1)))) |
|
691 (let (($x92 (and $x80 $x91))) |
|
692 (let (($x93 (or $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92))) |
|
693 (let (($x94 (and $x81 $x93))) |
|
694 (let (($x95 (or $x81 $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92 $x94))) |
|
695 (let (($x297 (not $x95))) |
|
696 (let (($x43 (bvule (_ bv256 16) w$))) |
|
697 (let (($x44 (not $x43))) |
|
698 (let ((@x63 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x44))) |
|
699 (let ((@x303 (unit-resolution ((_ th-lemma bv) (or $x43 $x297)) @x63 $x297))) |
|
700 (let ((@x26 (true-axiom true))) |
|
701 (let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81))) |
|
702 (let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300))) |
|
703 (unit-resolution @x314 @x322 false))))))))))))))))))))))))))))))))))))))))))))))))) |
|
704 |
|
705 024e51ae2c856c79195e59dfbc39c68dcf8ab939 29 0 |
|
706 unsat |
|
707 ((set-logic <null>) |
|
708 (proof |
|
709 (let ((?x28 (bv2int$ (_ bv0 2)))) |
|
710 (let (($x183 (<= ?x28 0))) |
|
711 (let (($x184 (not $x183))) |
|
712 (let (($x175 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0))) |
|
713 (let (($x53 (<= ?x47 0))) |
|
714 (not $x53))) :pattern ( (bv2int$ ?v0) ) :qid k!9)) |
|
715 )) |
|
716 (let (($x57 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0))) |
|
717 (let (($x53 (<= ?x47 0))) |
|
718 (not $x53))) :qid k!9)) |
|
719 )) |
|
720 (let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) |
|
721 (let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) |
|
722 (let (($x49 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0))) |
|
723 (< 0 ?x47)) :qid k!9)) |
|
724 )) |
|
725 (let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0)))))) |
|
726 (let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57))) |
|
727 (let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175))) |
|
728 (let (($x187 (not $x175))) |
|
729 (let (($x188 (or $x187 $x184))) |
|
730 (let ((@x189 ((_ quant-inst (_ bv0 2)) $x188))) |
|
731 (let (($x29 (= ?x28 0))) |
|
732 (let ((@x30 (asserted $x29))) |
|
733 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false))))))))))))))))))) |
|
734 |
|
735 20245d49b4c03da63c3124c5910beafc837f359a 12 0 |
|
736 unsat |
|
737 ((set-logic <null>) |
|
738 (proof |
|
739 (let ((?x31 (p$ true))) |
|
740 (let (($x29 (bvule (_ bv0 4) a$))) |
|
741 (let ((?x30 (p$ $x29))) |
|
742 (let (($x32 (= ?x30 ?x31))) |
|
743 (let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31))))) |
|
744 (let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true))))) |
|
745 (let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false)))) |
|
746 (mp (asserted (not $x32)) @x53 false)))))))))) |
|
747 |