equal
deleted
inserted
replaced
501 \ (! x y. P1 x & (P2 y|Q1 y) --> ~R x y) & \ |
501 \ (! x y. P1 x & (P2 y|Q1 y) --> ~R x y) & \ |
502 \ (! x y. P3 x & P4 y --> R x y) & \ |
502 \ (! x y. P3 x & P4 y --> R x y) & \ |
503 \ (! x y. P3 x & P5 y --> ~R x y) & \ |
503 \ (! x y. P3 x & P5 y --> ~R x y) & \ |
504 \ (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y)) \ |
504 \ (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y)) \ |
505 \ --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))"; |
505 \ --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))"; |
506 by (safe_meson_tac 1); (*40 secs*) |
506 by (safe_best_meson_tac 1); (*MUCH faster than iterative deepening*) |
507 result(); |
507 result(); |
508 |
508 |
509 (*The Los problem? Circulated by John Harrison*) |
509 (*The Los problem? Circulated by John Harrison*) |
510 Goal "(! x y z. P x y & P y z --> P x z) & \ |
510 Goal "(! x y z. P x y & P y z --> P x z) & \ |
511 \ (! x y z. Q x y & Q y z --> Q x z) & \ |
511 \ (! x y z. Q x y & Q y z --> Q x z) & \ |