Minlog loaded successfully
> ; ok, variable x: alpha added
; ok, variable y: alpha added
; ok, variable z: alpha added
> ; ok, predicate constant P: (arity) added
> ; ok, predicate constant Qpredconst: (arity alpha) added
> ; ok, predicate constant Rpredconst: (arity alpha alpha) added
> > > > > "Q x"
> "x R y"
> "Q17 x"
> > ; ?_1: (all x.Q1 x -> Q2 x) -> all x Q1 x -> all x Q2 x
> ; ok, we now have the new goal 
; ?_2: Q2 x from
;   1:all x.Q1 x -> Q2 x
;   2:all x Q1 x
;   x
> ; ok, ?_2 can be obtained from
; ?_3: Q1 x from
;   1:all x.Q1 x -> Q2 x
;   2:all x Q1 x
;   x
> ; ok, ?_3 is proved.  Proof finished.
> ; .....all x.Q1 x -> Q2 x by assumption u33
; .....x
; ....Q1 x -> Q2 x by all elim
; .....all x Q1 x by assumption u34
; .....x
; ....Q1 x by all elim
; ...Q2 x by imp elim
; ..all x Q2 x by all intro
; .all x Q1 x -> all x Q2 x by imp intro u34
; (all x.Q1 x -> Q2 x) -> all x Q1 x -> all x Q2 x by imp intro u33
> > ; ?_1: (all x.Q1 x -> Q2 x) -> all x Q1 x -> all x Q2 x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....all x.Q1 x -> Q2 x by assumption u38
; .....x
; ....Q1 x -> Q2 x by all elim
; .....all x Q1 x by assumption u39
; .....x
; ....Q1 x by all elim
; ...Q2 x by imp elim
; ..all x Q2 x by all intro
; .all x Q1 x -> all x Q2 x by imp intro u39
; (all x.Q1 x -> Q2 x) -> all x Q1 x -> all x Q2 x by imp intro u38
> > ; ?_1: (all x.Q1 x & Q2 x) -> all x Q1 x & all x Q2 x
> ; ok, we now have the new goal 
; ?_2: all x Q1 x & all x Q2 x from
;   1:all x.Q1 x & Q2 x
> ; ok, we now have the new goals 
; ?_4: all x Q2 x from
;   1:all x.Q1 x & Q2 x

; ?_3: all x Q1 x from
;   1:all x.Q1 x & Q2 x
> ; ok, we now have the new goal 
; ?_5: Q1 x from
;   1:all x.Q1 x & Q2 x
;   x
> ; ok, ?_5 is proved.  The active goal now is
; ?_4: all x Q2 x from
;   1:all x.Q1 x & Q2 x
> ; ok, we now have the new goal 
; ?_6: Q2 x from
;   1:all x.Q1 x & Q2 x
;   x
> ; ok, ?_6 is proved.  Proof finished.
> ; .....all x.Q1 x & Q2 x by assumption u44
; .....x
; ....Q1 x & Q2 x by all elim
; ...Q1 x by and elim left
; ..all x Q1 x by all intro
; .....all x.Q1 x & Q2 x by assumption u44
; .....x
; ....Q1 x & Q2 x by all elim
; ...Q2 x by and elim right
; ..all x Q2 x by all intro
; .all x Q1 x & all x Q2 x by and intro
; (all x.Q1 x & Q2 x) -> all x Q1 x & all x Q2 x by imp intro u44
> ; ?_1: (all x.Q1 x & Q2 x) -> all x Q1 x & all x Q2 x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....all x.Q1 x & Q2 x by assumption u47
; .....x
; ....Q1 x & Q2 x by all elim
; ...Q1 x by and elim left
; ..all x Q1 x by all intro
; .....all x.Q1 x & Q2 x by assumption u47
; .....x28
; ....Q1 x28 & Q2 x28 by all elim
; ...Q2 x28 by and elim right
; ..all x28 Q2 x28 by all intro
; .all x Q1 x & all x28 Q2 x28 by and intro
; (all x.Q1 x & Q2 x) -> all x Q1 x & all x28 Q2 x28 by imp intro u47
> > ; ?_1: all x Q1 x & all x Q2 x -> all x.Q1 x & Q2 x
> ; ok, we now have the new goal 
; ?_2: Q1 x & Q2 x from
;   1:all x Q1 x & all x Q2 x
;   x
> ; ok, we now have the new goals 
; ?_4: Q2 x from
;   1:all x Q1 x & all x Q2 x
;   x

; ?_3: Q1 x from
;   1:all x Q1 x & all x Q2 x
;   x
> ; ok, ?_3 is proved.  The active goal now is
; ?_4: Q2 x from
;   1:all x Q1 x & all x Q2 x
;   x
> ; ok, ?_4 is proved.  Proof finished.
> ; .....all x Q1 x & all x Q2 x by assumption u52
; ....all x Q1 x by and elim left
; ....x
; ...Q1 x by all elim
; .....all x Q1 x & all x Q2 x by assumption u52
; ....all x Q2 x by and elim right
; ....x
; ...Q2 x by all elim
; ..Q1 x & Q2 x by and intro
; .all x.Q1 x & Q2 x by all intro
; all x Q1 x & all x Q2 x -> all x.Q1 x & Q2 x by imp intro u52
> ; ?_1: all x Q1 x & all x Q2 x -> all x.Q1 x & Q2 x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....all x Q1 x & all x Q2 x by assumption u55
; ....all x Q1 x by and elim left
; ....x
; ...Q1 x by all elim
; .....all x Q1 x & all x Q2 x by assumption u55
; ....all x Q2 x by and elim right
; ....x
; ...Q2 x by all elim
; ..Q1 x & Q2 x by and intro
; .all x.Q1 x & Q2 x by all intro
; all x Q1 x & all x Q2 x -> all x.Q1 x & Q2 x by imp intro u55
> > ; ?_1: all x Q x -> exca x Q x
> ; ok, we now have the new goal 
; ?_2: F from
;   1:all x Q x
;   2:all x.Q x -> F
> ; ok, ?_2 can be obtained from
; ?_3: Q x from
;   1:all x Q x
;   2:all x.Q x -> F
;   x
> ; ok, ?_3 is proved.  Proof finished.
> ; ....all x.Q x -> F by assumption u61
; ....x
; ...Q x -> F by all elim
; ....all x Q x by assumption u60
; ....x
; ...Q x by all elim
; ..F by imp elim
; .exca x Q x by imp intro u61
; all x Q x -> exca x Q x by imp intro u60
> ; ?_1: all x Q x -> exca x Q x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....all x.Q x -> F by assumption u66
; ....x45
; ...Q x45 -> F by all elim
; ....all x Q x by assumption u65
; ....x45
; ...Q x45 by all elim
; ..F by imp elim
; .exca x Q x by imp intro u66
; all x Q x -> exca x Q x by imp intro u65
> ; ok, Symm has been added as a new global assumption.
> ; ok, Trans has been added as a new global assumption.
> ; ?_1: all x,y.x R y -> x R x
> ; ok, we now have the new goal 
; ?_2: x R x from
;   x  y  1:x R y
> ; ok, ?_2 can be obtained from
; ?_4: y R x from
;   x  y  1:x R y

; ?_3: x R y from
;   x  y  1:x R y
> ; ok, ?_3 is proved.  The active goal now is
; ?_4: y R x from
;   x  y  1:x R y
> ; ok, ?_4 can be obtained from
; ?_5: x R y from
;   x  y  1:x R y
> ; ok, ?_5 is proved.  Proof finished.
> ; ?_1: all x,y.x R y -> x R x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ........all x,y,z.x R y -> y R z -> x R z by global assumption Trans
; ........x
; .......all y,z.x R y -> y R z -> x R z by all elim
; .......y
; ......all z.x R y -> y R z -> x R z by all elim
; ......x
; .....x R y -> y R x -> x R x by all elim
; .....x R y by assumption u74
; ....y R x -> x R x by imp elim
; .......all x,y.x R y -> y R x by global assumption Symm
; .......x
; ......all y.x R y -> y R x by all elim
; ......y
; .....x R y -> y R x by all elim
; .....x R y by assumption u74
; ....y R x by imp elim
; ...x R x by imp elim
; ..x R y -> x R x by imp intro u74
; .all y.x R y -> x R x by all intro
; all x,y.x R y -> x R x by all intro
> > ; ?_1: (all x.((Q x -> F) -> F) -> Q x) -> (all x Q x -> P) -> exca x.Q x -> P
> ; ok, we now have the new goal 
; ?_2: F from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
> ; ok, ?_2 can be obtained from
; ?_3: Q x -> P from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x
> ; ok, we now have the new goal 
; ?_4: P from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
> ; ok, ?_4 can be obtained from
; ?_5: all x Q x from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
> ; ok, we now have the new goal 
; ?_6: Q x1 from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1
> ; ok, ?_6 can be obtained from
; ?_7: (Q x1 -> F) -> F from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1
> ; ok, we now have the new goal 
; ?_8: F from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
> ; ok, ?_8 can be obtained from
; ?_9: Q x1 -> P from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
> ; ok, we now have the new goal 
; ?_10: P from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
;   6:Q x1
> ; ok, ?_10 can be obtained from
; ?_11: all x Q x from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
;   6:Q x1
> ; ok, we now have the new goal 
; ?_12: Q x2 from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
;   6:Q x1
;   x2
> ; ok, ?_12 can be obtained from
; ?_13: (Q x2 -> F) -> F from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
;   6:Q x1
;   x2
> ; ok, we now have the new goal 
; ?_14: F from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
;   6:Q x1
;   x2  7:Q x2 -> F
> ; ok, ?_14 can be obtained from
; ?_15: Q x1 from
;   1:all x.((Q x -> F) -> F) -> Q x
;   2:all x Q x -> P
;   3:all x.(Q x -> P) -> F
;   x  4:Q x
;   x1  5:Q x1 -> F
;   6:Q x1
;   x2  7:Q x2 -> F
> ; ok, ?_15 is proved.  Proof finished.
> ; ?_1: (all x.((Q x -> F) -> F) -> Q x) -> (all x Q x -> P) -> exca x.Q x -> P
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....all x.(Q x -> P) -> F by assumption u102
; .....x
; ....(Q x -> P) -> F by all elim
; ......all x Q x -> P by assumption u101
; .........all x.((Q x -> F) -> F) -> Q x by assumption u100
; .........x95
; ........((Q x95 -> F) -> F) -> Q x95 by all elim
; ...........all x.(Q x -> P) -> F by assumption u102
; ...........x95
; ..........(Q x95 -> P) -> F by all elim
; ............all x Q x -> P by assumption u101
; ...............all x.((Q x -> F) -> F) -> Q x by assumption u100
; ...............x96
; ..............((Q x96 -> F) -> F) -> Q x96 by all elim
; ................Q x95 -> F by assumption u104
; ................Q x95 by assumption u105
; ...............F by imp elim
; ..............(Q x96 -> F) -> F by imp intro u106
; .............Q x96 by imp elim
; ............all x96 Q x96 by all intro
; ...........P by imp elim
; ..........Q x95 -> P by imp intro u105
; .........F by imp elim
; ........(Q x95 -> F) -> F by imp intro u104
; .......Q x95 by imp elim
; ......all x95 Q x95 by all intro
; .....P by imp elim
; ....Q x -> P by imp intro u103
; ...F by imp elim
; ..exca x.Q x -> P by imp intro u102
; .(all x Q x -> P) -> exca x.Q x -> P by imp intro u101
; (all x.((Q x -> F) -> F) -> Q x) -> (all x Q x -> P) -> exca x.Q x -> P by imp intro u100
> > ; ?_1: (P -> all y Q y) -> all y.P -> Q y
> ; ok, we now have the new goal 
; ?_2: Q y from
;   1:P -> all y Q y
;   y  2:P
> ; ok, ?_2 can be obtained from
; ?_3: P from
;   1:P -> all y Q y
;   y  2:P
> ; ok, ?_3 is proved.  Proof finished.
> ; ?_1: (P -> all y Q y) -> all y.P -> Q y
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....P -> all y Q y by assumption u114
; .....P by assumption u115
; ....all y Q y by imp elim
; ....y
; ...Q y by all elim
; ..P -> Q y by imp intro u115
; .all y.P -> Q y by all intro
; (P -> all y Q y) -> all y.P -> Q y by imp intro u114
> > ; ?_1: (exca x Q x -> P) -> all x.Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:exca x Q x -> P
;   x  2:Q x
> ; ok, ?_2 can be obtained from
; ?_3: exca x Q x from
;   1:exca x Q x -> P
;   x  2:Q x
> ; ok, we now have the new goal 
; ?_4: F from
;   1:exca x Q x -> P
;   x  2:Q x
;   3:all x.Q x -> F
> ; ok, ?_4 can be obtained from
; ?_5: Q x from
;   1:exca x Q x -> P
;   x  2:Q x
;   3:all x.Q x -> F
> ; ok, ?_5 is proved.  Proof finished.
> ; ?_1: (exca x Q x -> P) -> all x.Q x -> P
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....exca x Q x -> P by assumption u126
; .......all x.Q x -> F by assumption u128
; .......x
; ......Q x -> F by all elim
; ......Q x by assumption u127
; .....F by imp elim
; ....exca x Q x by imp intro u128
; ...P by imp elim
; ..Q x -> P by imp intro u127
; .all x.Q x -> P by all intro
; (exca x Q x -> P) -> all x.Q x -> P by imp intro u126
> > ; ?_1: (all y.F -> Q y) -> (P -> exca y Q y) -> exca y.P -> Q y
> ; ok, we now have the new goal 
; ?_2: F from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
> ; ok, ?_2 can be obtained from
; ?_3: P -> Q y from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y
> ; ok, we now have the new goal 
; ?_4: Q y from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
> ; ok, ?_4 can be obtained from
; ?_5: F from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
> ; ok, ?_5 can be obtained from
; ?_7: all y.Q y -> F from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P

; ?_6: P from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
> ; ok, ?_6 is proved.  The active goal now is
; ?_7: all y.Q y -> F from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
> ; ok, we now have the new goal 
; ?_8: F from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
;   y1  5:Q y1
> ; ok, ?_8 can be obtained from
; ?_9: P -> Q y1 from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
;   y1  5:Q y1
> ; ok, we now have the new goal 
; ?_10: Q y1 from
;   1:all y.F -> Q y
;   2:P -> exca y Q y
;   3:all y.(P -> Q y) -> F
;   y  4:P
;   y1  5:Q y1
;   6:P
> ; ok, ?_10 is proved.  Proof finished.
> ; ?_1: (all y.F -> Q y) -> (P -> exca y Q y) -> exca y.P -> Q y
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....all y.(P -> Q y) -> F by assumption u157
; .....y111
; ....(P -> Q y111) -> F by all elim
; .......all y.F -> Q y by assumption u155
; .......y111
; ......F -> Q y111 by all elim
; ........P -> exca y Q y by assumption u156
; ........P by assumption u158
; .......exca y Q y by imp elim
; ...........all y.(P -> Q y) -> F by assumption u157
; ...........y
; ..........(P -> Q y) -> F by all elim
; ...........Q y by assumption u159
; ..........P -> Q y by imp intro u160
; .........F by imp elim
; ........Q y -> F by imp intro u159
; .......all y.Q y -> F by all intro
; ......F by imp elim
; .....Q y111 by imp elim
; ....P -> Q y111 by imp intro u158
; ...F by imp elim
; ..exca y.P -> Q y by imp intro u157
; .(P -> exca y Q y) -> exca y.P -> Q y by imp intro u156
; (all y.F -> Q y) -> (P -> exca y Q y) -> exca y.P -> Q y by imp intro u155
> > ; ?_1: (((P -> F) -> F) -> P) -> (exca x.Q x -> P) -> all x Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
> ; ok, ?_2 can be obtained from
; ?_3: (P -> F) -> F from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
> ; ok, we now have the new goal 
; ?_4: F from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
;   4:P -> F
> ; ok, ?_4 can be obtained from
; ?_5: all x.(Q x -> P) -> F from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
;   4:P -> F
> ; ok, we now have the new goal 
; ?_6: F from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
;   4:P -> F
;   x  5:Q x -> P
> ; ok, ?_6 can be obtained from
; ?_7: P from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
;   4:P -> F
;   x  5:Q x -> P
> ; ok, ?_7 can be obtained from
; ?_8: Q x from
;   1:((P -> F) -> F) -> P
;   2:exca x.Q x -> P
;   3:all x Q x
;   4:P -> F
;   x  5:Q x -> P
> ; ok, ?_8 is proved.  Proof finished.
> ; ?_1: (((P -> F) -> F) -> P) -> (exca x.Q x -> P) -> all x Q x -> P
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....((P -> F) -> F) -> P by assumption u178
; ......P -> F by assumption u181
; .......((P -> F) -> F) -> P by assumption u178
; .........exca x.Q x -> P by assumption u179
; ............P -> F by assumption u182
; .............Q x -> P by assumption u183
; ..............all x Q x by assumption u180
; ..............x
; .............Q x by all elim
; ............P by imp elim
; ...........F by imp elim
; ..........(Q x -> P) -> F by imp intro u183
; .........all x.(Q x -> P) -> F by all intro
; ........F by imp elim
; .......(P -> F) -> F by imp intro u182
; ......P by imp elim
; .....F by imp elim
; ....(P -> F) -> F by imp intro u181
; ...P by imp elim
; ..all x Q x -> P by imp intro u180
; .(exca x.Q x -> P) -> all x Q x -> P by imp intro u179
; (((P -> F) -> F) -> P) -> (exca x.Q x -> P) -> all x Q x -> P by imp intro u178
> > ; ?_1: (all y.P -> Q y) -> P -> all y Q y
> ; ok, we now have the new goal 
; ?_2: Q y from
;   1:all y.P -> Q y
;   2:P
;   y
> ; ok, ?_2 can be obtained from
; ?_3: P from
;   1:all y.P -> Q y
;   2:P
;   y
> ; ok, ?_3 is proved.  Proof finished.
> ; ?_1: (all y.P -> Q y) -> P -> all y Q y
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; .....all y.P -> Q y by assumption u191
; .....y
; ....P -> Q y by all elim
; ....P by assumption u192
; ...Q y by imp elim
; ..all y Q y by all intro
; .P -> all y Q y by imp intro u192
; (all y.P -> Q y) -> P -> all y Q y by imp intro u191
> > ; ?_1: (((P -> F) -> F) -> P) -> (all x.Q x -> P) -> exca x Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
> ; ok, ?_2 can be obtained from
; ?_3: (P -> F) -> F from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
> ; ok, we now have the new goal 
; ?_4: F from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
;   4:P -> F
> ; ok, ?_4 can be obtained from
; ?_5: all x.Q x -> F from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
;   4:P -> F
> ; ok, we now have the new goal 
; ?_6: F from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
;   4:P -> F
;   x  5:Q x
> ; ok, ?_6 can be obtained from
; ?_7: P from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
;   4:P -> F
;   x  5:Q x
> ; ok, ?_7 can be obtained from
; ?_8: Q x from
;   1:((P -> F) -> F) -> P
;   2:all x.Q x -> P
;   3:exca x Q x
;   4:P -> F
;   x  5:Q x
> ; ok, ?_8 is proved.  Proof finished.
> ; ?_1: (((P -> F) -> F) -> P) -> (all x.Q x -> P) -> exca x Q x -> P
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....((P -> F) -> F) -> P by assumption u210
; ......P -> F by assumption u213
; .......((P -> F) -> F) -> P by assumption u210
; .........exca x Q x by assumption u212
; ............P -> F by assumption u214
; ..............all x.Q x -> P by assumption u211
; ..............x
; .............Q x -> P by all elim
; .............Q x by assumption u215
; ............P by imp elim
; ...........F by imp elim
; ..........Q x -> F by imp intro u215
; .........all x.Q x -> F by all intro
; ........F by imp elim
; .......(P -> F) -> F by imp intro u214
; ......P by imp elim
; .....F by imp elim
; ....(P -> F) -> F by imp intro u213
; ...P by imp elim
; ..exca x Q x -> P by imp intro u212
; .(all x.Q x -> P) -> exca x Q x -> P by imp intro u211
; (((P -> F) -> F) -> P) -> (all x.Q x -> P) -> exca x Q x -> P by imp intro u210
> > ; ?_1: (exca y.P -> Q y) -> P -> exca y Q y
> ; ok, we now have the new goal 
; ?_2: F from
;   1:exca y.P -> Q y
;   2:P
;   3:all y.Q y -> F
> ; ok, ?_2 can be obtained from
; ?_3: all y.(P -> Q y) -> F from
;   1:exca y.P -> Q y
;   2:P
;   3:all y.Q y -> F
> ; ok, we now have the new goal 
; ?_4: F from
;   1:exca y.P -> Q y
;   2:P
;   3:all y.Q y -> F
;   y  4:P -> Q y
> ; ok, ?_4 can be obtained from
; ?_5: Q y from
;   1:exca y.P -> Q y
;   2:P
;   3:all y.Q y -> F
;   y  4:P -> Q y
> ; ok, ?_5 can be obtained from
; ?_6: P from
;   1:exca y.P -> Q y
;   2:P
;   3:all y.Q y -> F
;   y  4:P -> Q y
> ; ok, ?_6 is proved.  Proof finished.
> ; ?_1: (exca y.P -> Q y) -> P -> exca y Q y
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....exca y.P -> Q y by assumption u229
; ........all y.Q y -> F by assumption u231
; ........y
; .......Q y -> F by all elim
; ........P -> Q y by assumption u232
; ........P by assumption u230
; .......Q y by imp elim
; ......F by imp elim
; .....(P -> Q y) -> F by imp intro u232
; ....all y.(P -> Q y) -> F by all intro
; ...F by imp elim
; ..exca y Q y by imp intro u231
; .P -> exca y Q y by imp intro u230
; (exca y.P -> Q y) -> P -> exca y Q y by imp intro u229
> > ; ?_1: (all y.((Q y -> F) -> F) -> Q y) -> exca x.Q x -> all y Q y
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....all x.(Q x -> all y Q y) -> F by assumption u243
; ....x
; ...(Q x -> all y Q y) -> F by all elim
; .......all y.((Q y -> F) -> F) -> Q y by assumption u242
; .......y
; ......((Q y -> F) -> F) -> Q y by all elim
; .........all x.(Q x -> all y Q y) -> F by assumption u243
; .........y
; ........(Q y -> all y Q y) -> F by all elim
; ............all y.((Q y -> F) -> F) -> Q y by assumption u242
; ............y179
; ...........((Q y179 -> F) -> F) -> Q y179 by all elim
; .............Q y -> F by assumption u245
; .............Q y by assumption u246
; ............F by imp elim
; ...........(Q y179 -> F) -> F by imp intro u247
; ..........Q y179 by imp elim
; .........all y179 Q y179 by all intro
; ........Q y -> all y179 Q y179 by imp intro u246
; .......F by imp elim
; ......(Q y -> F) -> F by imp intro u245
; .....Q y by imp elim
; ....all y Q y by all intro
; ...Q x -> all y Q y by imp intro u244
; ..F by imp elim
; .exca x.Q x -> all y Q y by imp intro u243
; (all y.((Q y -> F) -> F) -> Q y) -> exca x.Q x -> all y Q y by imp intro u242
> > ; ?_1: (ex x.Q1 x & Q2 x) -> ex x Q1 x & ex x Q2 x
> ; ok, we now have the new goal 
; ?_2: ex x Q1 x & ex x Q2 x from
;   1:ex x.Q1 x & Q2 x
> ; ok, we now have the new goals 
; ?_4: ex x Q2 x from
;   1:ex x.Q1 x & Q2 x

; ?_3: ex x Q1 x from
;   1:ex x.Q1 x & Q2 x
> ; ok, ?_3 can be obtained from
; ?_5: all x181.Q1 x181 & Q2 x181 -> ex x Q1 x from
;   1:ex x.Q1 x & Q2 x
> ; ok, we now have the new goal 
; ?_6: ex x Q1 x from
;   1:ex x.Q1 x & Q2 x
;   x  2:Q1 x & Q2 x
> ; ok, ?_6 can be obtained from
; ?_7: Q1 x from
;   1:ex x.Q1 x & Q2 x
;   x  2:Q1 x & Q2 x
> ; ok, ?_7 is proved.  The active goal now is
; ?_4: ex x Q2 x from
;   1:ex x.Q1 x & Q2 x
> ; ok, ?_4 can be obtained from
; ?_8: all x185.Q1 x185 & Q2 x185 -> ex x Q2 x from
;   1:ex x.Q1 x & Q2 x
> ; ok, we now have the new goal 
; ?_9: ex x Q2 x from
;   1:ex x.Q1 x & Q2 x
;   x  2:Q1 x & Q2 x
> ; ok, ?_9 can be obtained from
; ?_10: Q2 x from
;   1:ex x.Q1 x & Q2 x
;   x  2:Q1 x & Q2 x
> ; ok, ?_10 is proved.  Proof finished.
> ; ?_1: (ex x.Q1 x & Q2 x) -> ex x Q1 x & ex x Q2 x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....(ex x220.Q1 x220 & Q2 x220) -> (all x220.Q1 x220 & Q2 x220 -> ex x Q1 x) -> ex x Q1 x by axiom Ex-Elim
; ....ex x.Q1 x & Q2 x by assumption u264
; ...(all x220.Q1 x220 & Q2 x220 -> ex x Q1 x) -> ex x Q1 x by imp elim
; .......all x222.Q1 x222 -> ex x222 Q1 x222 by axiom Ex-Intro
; .......x220
; ......Q1 x220 -> ex x222 Q1 x222 by all elim
; .......Q1 x220 & Q2 x220 by assumption u266
; ......Q1 x220 by and elim left
; .....ex x222 Q1 x222 by imp elim
; ....Q1 x220 & Q2 x220 -> ex x222 Q1 x222 by imp intro u266
; ...all x220.Q1 x220 & Q2 x220 -> ex x222 Q1 x222 by all intro
; ..ex x Q1 x by imp elim
; ....(ex x216.Q1 x216 & Q2 x216) -> (all x216.Q1 x216 & Q2 x216 -> ex x Q2 x) -> ex x Q2 x by axiom Ex-Elim
; ....ex x.Q1 x & Q2 x by assumption u264
; ...(all x216.Q1 x216 & Q2 x216 -> ex x Q2 x) -> ex x Q2 x by imp elim
; .......all x218.Q2 x218 -> ex x218 Q2 x218 by axiom Ex-Intro
; .......x216
; ......Q2 x216 -> ex x218 Q2 x218 by all elim
; .......Q1 x216 & Q2 x216 by assumption u265
; ......Q2 x216 by and elim right
; .....ex x218 Q2 x218 by imp elim
; ....Q1 x216 & Q2 x216 -> ex x218 Q2 x218 by imp intro u265
; ...all x216.Q1 x216 & Q2 x216 -> ex x218 Q2 x218 by all intro
; ..ex x Q2 x by imp elim
; .ex x Q1 x & ex x Q2 x by and intro
; (ex x.Q1 x & Q2 x) -> ex x Q1 x & ex x Q2 x by imp intro u264
> "[x0]x0@x0"
> > ; ?_1: ex x Q x & P -> ex x.Q x & P
> ; ok, we now have the new goal 
; ?_2: ex x.Q x & P from
;   1:ex x Q x & P
> ; ok, ?_2 can be obtained from
; ?_3: ex x.Q x & P from
;   1:ex x Q x & P
;   2:ex x Q x
> ; ok, ?_3 can be obtained from
; ?_4: all x227.Q x227 -> ex x.Q x & P from
;   1:ex x Q x & P
;   2:ex x Q x
> ; ok, we now have the new goal 
; ?_5: ex x.Q x & P from
;   1:ex x Q x & P
;   2:ex x Q x
;   x  3:Q x
> ; ok, ?_5 can be obtained from
; ?_6: Q x & P from
;   1:ex x Q x & P
;   2:ex x Q x
;   x  3:Q x
> ; ok, we now have the new goals 
; ?_8: P from
;   1:ex x Q x & P
;   2:ex x Q x
;   x  3:Q x

; ?_7: Q x from
;   1:ex x Q x & P
;   2:ex x Q x
;   x  3:Q x
> ; ok, ?_7 is proved.  The active goal now is
; ?_8: P from
;   1:ex x Q x & P
;   2:ex x Q x
;   x  3:Q x
> ; ok, ?_8 is proved.  Proof finished.
> ; ?_1: ex x Q x & P -> ex x.Q x & P
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ...ex x242 Q x242 -> (all x242.Q x242 -> ex x.Q x & P) -> ex x.Q x & P by axiom Ex-Elim
; ....ex x Q x & P by assumption u280
; ...ex x Q x by and elim left
; ..(all x242.Q x242 -> ex x.Q x & P) -> ex x.Q x & P by imp elim
; ......all x244.Q x244 & P -> ex x244.Q x244 & P by axiom Ex-Intro
; ......x242
; .....Q x242 & P -> ex x244.Q x244 & P by all elim
; ......Q x242 by assumption u281
; .......ex x Q x & P by assumption u280
; ......P by and elim right
; .....Q x242 & P by and intro
; ....ex x244.Q x244 & P by imp elim
; ...Q x242 -> ex x244.Q x244 & P by imp intro u281
; ..all x242.Q x242 -> ex x244.Q x244 & P by all intro
; .ex x.Q x & P by imp elim
; ex x Q x & P -> ex x.Q x & P by imp intro u280
> "[x0]x0"
> > ; ?_1: all x Q x -> ex x Q x
> ; ok, we now have the new goal 
; ?_2: ex x Q x from
;   1:all x Q x
> ; ok, ?_2 can be obtained from
; ?_3: Q x from
;   1:all x Q x
;   x
> ; ok, ?_3 is proved.  Proof finished.
> ; ?_1: all x Q x -> ex x Q x
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ...all x255.Q x255 -> ex x255 Q x255 by axiom Ex-Intro
; ...x
; ..Q x -> ex x255 Q x255 by all elim
; ...all x Q x by assumption u287
; ...x
; ..Q x by all elim
; .ex x255 Q x255 by imp elim
; all x Q x -> ex x255 Q x255 by imp intro u287
> "x"
> > ; ?_1: (ex x Q x -> P) -> all x.Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:ex x Q x -> P
;   x  2:Q x
> ; ok, ?_2 can be obtained from
; ?_3: ex x Q x from
;   1:ex x Q x -> P
;   x  2:Q x
> ; ok, ?_3 can be obtained from
; ?_4: Q x from
;   1:ex x Q x -> P
;   x  2:Q x
> ; ok, ?_4 is proved.  Proof finished.
> ; ?_1: (ex x Q x -> P) -> all x.Q x -> P
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....ex x Q x -> P by assumption u296
; ......all x264.Q x264 -> ex x264 Q x264 by axiom Ex-Intro
; ......x
; .....Q x -> ex x264 Q x264 by all elim
; .....Q x by assumption u297
; ....ex x264 Q x264 by imp elim
; ...P by imp elim
; ..Q x -> P by imp intro u297
; .all x.Q x -> P by all intro
; (ex x Q x -> P) -> all x.Q x -> P by imp intro u296
> > ; ?_1: (ex x.Q x -> P) -> all x Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:ex x.Q x -> P
;   2:all x Q x
> ; ok, ?_2 can be obtained from
; ?_3: all x266.(Q x266 -> P) -> P from
;   1:ex x.Q x -> P
;   2:all x Q x
> ; ok, we now have the new goal 
; ?_4: P from
;   1:ex x.Q x -> P
;   2:all x Q x
;   x  3:Q x -> P
> ; ok, ?_4 can be obtained from
; ?_5: Q x from
;   1:ex x.Q x -> P
;   2:all x Q x
;   x  3:Q x -> P
> ; ok, ?_5 is proved.  Proof finished.
> ; ?_1: (ex x.Q x -> P) -> all x Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:ex x.Q x -> P
;   2:all x Q x
> ; ok, ?_2 can be obtained from
; ?_3: all x269.(Q x269 -> P) -> P from
;   1:ex x.Q x -> P
;   2:all x Q x
> ; ok, ?_3 is proved by minimal quantifier logic.  Proof finished.
> ; ....(ex x276.Q x276 -> P) -> (all x276.(Q x276 -> P) -> P) -> P by axiom Ex-Elim
; ....ex x.Q x -> P by assumption u310
; ...(all x276.(Q x276 -> P) -> P) -> P by imp elim
; ......Q x276 -> P by assumption u312
; .......all x Q x by assumption u311
; .......x276
; ......Q x276 by all elim
; .....P by imp elim
; ....(Q x276 -> P) -> P by imp intro u312
; ...all x276.(Q x276 -> P) -> P by all intro
; ..P by imp elim
; .all x Q x -> P by imp intro u311
; (ex x.Q x -> P) -> all x Q x -> P by imp intro u310
> > ; ?_1: (all x.Q x -> P) -> ex x Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:all x.Q x -> P
;   2:ex x Q x
> ; ok, ?_2 can be obtained from
; ?_3: all x278.Q x278 -> P from
;   1:all x.Q x -> P
;   2:ex x Q x
> ; ok, ?_3 is proved.  Proof finished.
> ; ?_1: (all x.Q x -> P) -> ex x Q x -> P
> ; ok, we now have the new goal 
; ?_2: P from
;   1:all x.Q x -> P
;   2:ex x Q x
> ; ok, ?_2 can be obtained from
; ?_3: all x281.Q x281 -> P from
;   1:all x.Q x -> P
;   2:ex x Q x
> ; ok, ?_3 is proved by minimal quantifier logic.  Proof finished.
> > ; ?_1: (ex y.P -> Q y) -> P -> ex y Q y
> ; ok, we now have the new goal 
; ?_2: ex y Q y from
;   1:ex y.P -> Q y
;   2:P
> ; ok, ?_2 can be obtained from
; ?_3: all x283.(P -> Q x283) -> ex y Q y from
;   1:ex y.P -> Q y
;   2:P
> ; ok, we now have the new goal 
; ?_4: ex y Q y from
;   1:ex y.P -> Q y
;   2:P
;   x  3:P -> Q x
> ; ok, ?_4 can be obtained from
; ?_5: Q x from
;   1:ex y.P -> Q y
;   2:P
;   x  3:P -> Q x
> ; ok, ?_5 can be obtained from
; ?_6: P from
;   1:ex y.P -> Q y
;   2:P
;   x  3:P -> Q x
> ; ok, ?_6 is proved.  Proof finished.
> ; ?_1: (ex y.P -> Q y) -> P -> ex y Q y
> ; ok, ?_1 is proved by minimal quantifier logic.  Proof finished.
> ; ....(ex x299.P -> Q x299) -> (all x299.(P -> Q x299) -> ex y Q y) -> ex y Q y by axiom Ex-Elim
; ....ex y.P -> Q y by assumption u334
; ...(all x299.(P -> Q x299) -> ex y Q y) -> ex y Q y by imp elim
; .......all x301.Q x301 -> ex x301 Q x301 by axiom Ex-Intro
; .......x299
; ......Q x299 -> ex x301 Q x301 by all elim
; .......P -> Q x299 by assumption u336
; .......P by assumption u335
; ......Q x299 by imp elim
; .....ex x301 Q x301 by imp elim
; ....(P -> Q x299) -> ex x301 Q x301 by imp intro u336
; ...all x299.(P -> Q x299) -> ex x301 Q x301 by all intro
; ..ex y Q y by imp elim
; .P -> ex y Q y by imp intro u335
; (ex y.P -> Q y) -> P -> ex y Q y by imp intro u334
> "[x0]x0"
>