;(in-package "OSCAR")

(setf *problems*
         (eval-when (:compile-toplevel :execute)
             (make-problem-list
               "
Problem #1
This is a case of collective rebutting defeat
Given premises:
     P    justification = 1.0
     A    justification = 1.0
Ultimate epistemic interests:
     R    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> Q   strength = 1.0
      pf-reason_2:   {Q} ||=> R   strength = 1.0
      pf-reason_3:   {C} ||=> ~R   strength = 1.0
      pf-reason_4:   {B} ||=> C   strength = 1.0
      pf-reason_5:   {A} ||=> B   strength = 1.0

               Problem #2
This is the same as #1 except that some reasons are backwards.
Given premises:
     P    justification = 1.0
     A    justification = 1.0
Ultimate epistemic interests:
     R    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> Q   strength = 1.0
      pf-reason_2:   {Q} ||=> R   strength = 1.0
      pf-reason_3:   {A} ||=> B   strength = 1.0

    BACKWARDS PRIMA FACIE REASONS
      pf-reason_4:   {} {C} ||=> ~R   strength = 1.0
      pf-reason_5:   {} {B} ||=> C   strength = 1.0

Problem #3
Figure 2
Given premises:
     A    justification = 1.0
     B    justification = 1.0
     C    justification = 1.0
Ultimate epistemic interests:
     J    interest = 1.0
     K    interest = 1.0
     L    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A} ||=> D   strength = 1.0
      pf-reason_2:   {D} ||=> G   strength = 1.0
      pf-reason_3:   {B} ||=> E   strength = 1.0
      pf-reason_4:   {C} ||=> F   strength = 1.0
      pf-reason_5:   {I} ||=> L   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {G} ||=> J   strength = 1.0
      con-reason_2:   {E} ||=> H   strength = 1.0
      con-reason_3:   {H} ||=> K   strength = 1.0
      con-reason_4:   {F} ||=> I   strength = 1.0
      con-reason_5:   {F} ||= > (B @ E)   strength = 1.0
      con-reason_6:   {H} ||=> (D @ G)   strength = 1.0

Problem #4
Figure 3
Given premises:
     A    justification = 1.0
     B    justification = 1.0
Ultimate epistemic interests:
     J    interest = 1.0
     K    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A} ||=> D   strength = 1.0
      pf-reason_2:   {D} ||=> G   strength = 1.0
      pf-reason_3:   {B} ||=> ~D   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {G} ||=> J   strength = 1.0
      con-reason_2:   {~D} ||=> H   strength = 1.0
      con-reason_3:   {H} ||=> K   strength = 1.0

Problem #5
Figure 4
Given premises:
     A    justification = 1.0
     B    justification = 1.0
     C    justification = 1.0
Ultimate epistemic interests:
     J    interest = 1.0
     K    interest = 1.0
     L    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A} ||=> D   strength = 1.0
      pf-reason_2:   {D} ||=> G   strength = 1.0
      pf-reason_3:   {B} ||=> ~D   strength = 1.0
      pf-reason_4:   {C} ||=> D   strength = 1.0
      pf-reason_5:   {I} ||=> L   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {G} ||=> J   strength = 1.0
      con-reason_2:   {~D} ||=> H   strength = 1.0
      con-reason_3:   {H} ||=> K   strength = 1.0
      con-reason_4:   {D} ||=> I   strength = 1.0

Problem #6
Figure 5
Given premises:
     A    justification = 1.0
     B    justification = 1.0
     C    justification = 1.0
Ultimate epistemic interests:
     J    interest = 1.0
     K    interest = 1.0
     L    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A} ||=> D   strength = 1.0
      pf-reason_2:   {D} ||=> G   strength = 1.0
      pf-reason_3:   {B} ||=> ~D   strength = 1.0
      pf-reason_4:   {C} ||=> F   strength = 1.0
      pf-reason_5:   {I} ||=> L   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {G} ||=> J   strength = 1.0
      con-reason_2:   {~D} ||=> H   strength = 1.0
      con-reason_3:   {H} ||=> K   strength = 1.0
      con-reason_4:   {F} ||=> I   strength = 1.0
      con-reason_5:   {~D} ||=> M   strength = 1.0
      con-reason_6:   {M} ||=> N   strength = 1.0
      con-reason_7:   {N} ||=> (C @ F)   strength = 1.0
      con-reason_8:   {F} ||=> (B @ ~D)   strength = 1.0

Problem #7
Figure 7 -- self-defeat
Given premises:
     P    justification = 1.0
     Q    justification = 1.0
     S    justification = 1.0
Ultimate epistemic interests:
     T    interest = 1.0
     (R v ~T)    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> R   strength = 1.0
      pf-reason_2:   {Q} ||=> ~R   strength = 1.0
      pf-reason_3:   {S} ||=> T   strength = 1.0

Problem #8
Figure 8 -- the lottery paradox paradox
Given premises:
     P    justification = 1.0
Ultimate epistemic interests:
     ~T1    interest = 1.0
     ~T2    interest = 1.0
     ~T3    interest = 1.0
     R    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {R} ||=> ~T1   strength = 1.0
      pf-reason_2:   {R} ||=> ~T2   strength = 1.0
      pf-reason_3:   {R} ||=> ~T3   strength = 1.0
      pf-reason_4:   {P} ||=> R   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {R , ~T1 , ~T2} ||=> T3   strength = 1.0
      con-reason_2:   {R , ~T2 , ~T3} ||=> T1   strength = 1.0
      con-reason_3:   {R , ~T1 , ~T3} ||=> T2   strength = 1.0
      con-reason_4:   {~T1 , ~T2 , ~T3} ||=> ~R   strength = 1.0

Problem #9
Figure 8 -- the lottery paradox paradox using logic
Given premises:
     P    justification = 1.0
Ultimate epistemic interests:
     ~T1    interest = 1.0
     ~T2    interest = 1.0
     ~T3    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {R} ||=> ~T1   strength = 1.0
      pf-reason_2:   {R} ||=> ~T2   strength = 1.0
      pf-reason_3:   {R} ||=> ~T3   strength = 1.0
      pf-reason_4:   {P} ||=> R   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {R} ||=> (T1 v (T2 v T3))   strength = 1.0

Problem #10
Figure 9 -- No nearest defeasible ancestor is defeated.
Given premises:
     P    justification = 1.0
Ultimate epistemic interests:
     R    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> Q   strength = 1.0
      pf-reason_2:   {Q} ||=> R   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {R} ||=> (P @ Q)   strength = 1.0

Problem #11
figure 10 -- Robert and the pink elephant.
Given premises:
     P    justification = 1.0
     Q    justification = 1.0
     R    justification = 1.0
Ultimate epistemic interests:
     U    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P , Q} ||=> S   strength = 1.0
      pf-reason_2:   {R} ||=> T   strength = 1.0
      pf-reason_3:   {S} ||=> U   strength = 1.0
      pf-reason_4:   {V} ||=> ((P & Q) @ S)   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {T , U} ||=> V   strength = 1.0

Problem #12
figure 11 -- a simple case of ancestor defeat.
Given premises:
     P    justification = 1.0
     Q    justification = 1.0
     R    justification = 1.0
Ultimate epistemic interests:
     W    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> S   strength = 1.0
      pf-reason_2:   {S} ||=> U   strength = 1.0
      pf-reason_3:   {Q} ||=> T   strength = 1.0
      pf-reason_4:   {R} ||=> W   strength = 1.0
      pf-reason_5:   {V} ||=> (S @ U)   strength = 1.0
      pf-reason_6:   {U} ||=> (R @ W)   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {S , T} ||=> V   strength = 1.0

Problem #13
figure 12 -- a more complicated case of ancestor defeat.
Given premises:
     P    justification = 1.0
     Q    justification = 1.0
     R    justification = 1.0
     X    justification = 1.0
Ultimate epistemic interests:
     W    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> S   strength = 1.0
      pf-reason_2:   {S} ||=> U   strength = 1.0
      pf-reason_3:   {Q} ||=> T   strength = 1.0
      pf-reason_4:   {R} ||=> W   strength = 1.0
      pf-reason_5:   {X} ||=> ~S   strength = 1.0
      pf-reason_6:   {V} ||=> (S @ U)   strength = 1.0
      pf-reason_7:   {U} ||=> (R @ W)   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {S , T} ||=> V   strength = 1.0

Problem #14
figure 13 -- a still more complicated case of ancestor defeat.
Given premises:
     P    justification = 1.0
     Q    justification = 1.0
     R    justification = 1.0
     X    justification = 1.0
Ultimate epistemic interests:
     W    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P} ||=> S   strength = 1.0
      pf-reason_2:   {S} ||=> U   strength = 1.0
      pf-reason_3:   {Q} ||=> T   strength = 1.0
      pf-reason_4:   {R} ||=> W   strength = 1.0
      pf-reason_5:   {S} ||=> Y   strength = 1.0
      pf-reason_6:   {X} ||=> ~S   strength = 1.0
      pf-reason_7:   {V} ||=> (S @ U)   strength = 1.0
      pf-reason_8:   {U} ||=> (R @ W)   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {Y , T} ||=> V   strength = 1.0

Problem #15
figure 14 -- a three-membered defeat cycle.
Given premises:
     A    justification = 1.0
     P    justification = 1.0
     R    justification = 1.0
     T    justification = 1.0
Ultimate epistemic interests:
     B    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A} ||=> B   strength = 1.0
      pf-reason_2:   {P} ||=> Q   strength = 1.0
      pf-reason_3:   {R} ||=> S   strength = 1.0
      pf-reason_4:   {T} ||=> U   strength = 1.0
      pf-reason_5:   {Q} ||=> (R @ S)   strength = 1.0
      pf-reason_6:   {S} ||=> (T @ U)   strength = 1.0
      pf-reason_7:   {U} ||=> (P @ Q)   strength = 1.0
      pf-reason_8:   {Q} ||=> (A @ B)   strength = 1.0

Problem #16
figure 18 -- the paradox of the preface.
Given premises:
     P1    justification = 1.0
     P2    justification = 1.0
     P3    justification = 1.0
     S    justification = 1.0
     T    justification = 1.0
Ultimate epistemic interests:
     (Q1 & (Q2 & Q3))    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P1} ||=> Q1   strength = 1.0
      pf-reason_2:   {P2} ||=> Q2   strength = 1.0
      pf-reason_3:   {P3} ||=> Q3   strength = 1.0
      pf-reason_4:   {S} ||=> R   strength = 1.0
      pf-reason_5:   {T} ||=> ~(Q1 & (Q2 & Q3))   strength = 1.0
      pf-reason_6:   {S1} ||=> (T @ ~(Q1 & (Q2 & Q3)))   strength = 1.0
      pf-reason_7:   {S2} ||=> (T @ ~(Q1 & (Q2 & Q3)))   strength = 1.0
      pf-reason_8:   {S3} ||=> (T @ ~(Q1 & (Q2 & Q3)))   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {Q1 , Q2} ||=> (Q1 & Q2)   strength = 1.0
      con-reason_2:   {Q2 , Q3} ||=> (Q2 & Q3)   strength = 1.0
      con-reason_3:   {Q1 , Q3} ||=> (Q1 & Q3)   strength = 1.0
      con-reason_4:   {R , (Q1 & Q3)} ||=> S2   strength = 1.0
      con-reason_5:   {R , (Q2 & Q3)} ||=> S1   strength = 1.0
      con-reason_6:   {R , (Q1 & Q2)} ||=> S3   strength = 1.0
      con-reason_7:   {(Q1 & Q2) , ~(Q1 & (Q2 & Q3))} ||=> ~Q3   strength = 1.0
      con-reason_8:   {(Q2 & Q3) , ~(Q1 & (Q2 & Q3))} ||=> ~Q1   strength = 1.0
      con-reason_9:   {(Q1 & Q3) , ~(Q1 & (Q2 & Q3))} ||=> ~Q2   strength = 1.0

    BACKWARDS CONCLUSIVE REASONS
      con-reason_11:   {} {Q1 , Q2 , Q3} ||=> (Q1 & (Q2 & Q3))   strength = 1.0

Problem #17
figure 18 -- the paradox of the preface, using logic.
Given premises:
     P1    justification = 1.0
     P2    justification = 1.0
     P3    justification = 1.0
     S    justification = 1.0
     T    justification = 1.0
Ultimate epistemic interests:
     (Q1 & (Q2 & Q3))    interest = 1.0

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {P1} ||=> Q1   strength = 1.0
      pf-reason_2:   {P2} ||=> Q2   strength = 1.0
      pf-reason_3:   {P3} ||=> Q3   strength = 1.0
      pf-reason_4:   {S} ||=> R   strength = 1.0
      pf-reason_5:   {T} ||=> ~(Q1 & (Q2 & Q3))   strength = 1.0
      pf-reason_6:   {S1} ||=> (T @ ~(Q1 & (Q2 & Q3)))   strength = 1.0
      pf-reason_7:   {S2} ||=> (T @ ~(Q1 & (Q2 & Q3)))   strength = 1.0
      pf-reason_8:   {S3} ||=> (T @ ~(Q1 & (Q2 & Q3)))   strength = 1.0

    FORWARDS CONCLUSIVE REASONS
      con-reason_4:   {R , Q1 , Q3} ||=> S2   strength = 1.0
      con-reason_5:   {R , Q2 , Q3} ||=> S1   strength = 1.0
      con-reason_6:   {R , Q1 , Q2} ||=> S3   strength = 1.0

Problem #18
This uses contradiction-inversion.
Given premises:
     B    justification = 1
     A    justification = 1
     C    justification = 1
Ultimate epistemic interests:
     Q    interest = .7

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A , B} ||=> P   strength = .7
      pf-reason_2:   {C} ||=> ~Q   strength = .8

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {P} ||=> Q   strength = 1.0

Problem #19
Four-way collective defeat.
Given premises:
     A1    justification = 1
     B1    justification = 1
     C1    justification = 1
     D1    justification = 1
Ultimate epistemic interests:
     P1    interest = .7
     Q1    interest = .7
     R1    interest = .7
     S1    interest = .7

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A1} ||=> P1   strength = .7
      pf-reason_2:   {B1} ||=> Q1   strength = .7
      pf-reason_3:   {C1} ||=> R1   strength = .7
      pf-reason_4:   {D1} ||=> S1   strength = .7

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {P1,Q1,R1} ||=> ~S1   strength = 1.0
      con-reason_2:   {P1,Q1,S1} ||=> ~R1   strength = 1.0
      con-reason_3:   {S1,Q1,R1} ||=> ~P1   strength = 1.0
      con-reason_4:   {P1,S1,R1} ||=> ~Q1   strength = 1.0

Problem #20
Two copies of four-way collective defeat.
Given premises:
     A1    justification = 1
     B1    justification = 1
     C1    justification = 1
     D1    justification = 1
     A2    justification = 1
     B2    justification = 1
     C2    justification = 1
     D2    justification = 1
Ultimate epistemic interests:
     P1    interest = .7
     Q1    interest = .7
     R1    interest = .7
     S1    interest = .7
     P2    interest = .7
     Q2    interest = .7
     R2    interest = .7
     S2    interest = .7

    FORWARDS PRIMA FACIE REASONS
      pf-reason_1:   {A1} ||=> P1   strength = .7
      pf-reason_2:   {B1} ||=> Q1   strength = .7
      pf-reason_3:   {C1} ||=> R1   strength = .7
      pf-reason_4:   {D1} ||=> S1   strength = .7
      pf-reason_5:   {A2} ||=> P2   strength = .7
      pf-reason_6:   {B2} ||=> Q2   strength = .7
      pf-reason_7:   {C2} ||=> R2   strength = .7
      pf-reason_8:   {D2} ||=> S2   strength = .7

    FORWARDS CONCLUSIVE REASONS
      con-reason_1:   {P1,Q1,R1} ||=> ~S1   strength = 1.0
      con-reason_2:   {P1,Q1,S1} ||=> ~R1   strength = 1.0
      con-reason_3:   {S1,Q1,R1} ||=> ~P1   strength = 1.0
      con-reason_4:   {P1,S1,R1} ||=> ~Q1   strength = 1.0
      con-reason_5:   {P2,Q2,R2} ||=> ~S2   strength = 1.0
      con-reason_6:   {P2,Q2,S2} ||=> ~R2   strength = 1.0
      con-reason_7:   {S2,Q2,R2} ||=> ~P2   strength = 1.0
      con-reason_8:   {P2,S2,R2} ||=> ~Q2   strength = 1.0

Problem #21

Given premises:
Ultimate epistemic interests:
     ((p -> q) <-> (~q -> ~p))    interest = 1.0

Problem #22

Given premises:
Ultimate epistemic interests:
     (~~p <-> p)    interest = 1.0

Problem #23

Given premises:
Ultimate epistemic interests:
     (~(p -> q) -> (q -> p))    interest = 1.0

Problem #24

Given premises:
Ultimate epistemic interests:
     ((~p -> q) <-> (~q -> p))    interest = 1.0

Problem #25

Given premises:
Ultimate epistemic interests:
     (((p v q) -> (p v r)) -> (p v (q -> r)))    interest = 1.0

Problem #26

Given premises:
Ultimate epistemic interests:
     (p v ~p)    interest = 1.0

Problem #27

Given premises:
Ultimate epistemic interests:
     (p v ~~~p)    interest = 1.0

Problem #28

Given premises:
Ultimate epistemic interests:
     (((p -> q) -> p) -> p)    interest = 1.0

Problem #29

Given premises:
Ultimate epistemic interests:
     (((p v q) & ((~p v q) & (p v ~q))) -> ~(~p v ~q))    interest = 1.0

Problem #30

Given premises:
     (q -> r)    justification = 1.0
     (r -> (p & q))    justification = 1.0
     (p -> (q v r))    justification = 1.0
Ultimate epistemic interests:
     (p <-> q)    interest = 1.0

Problem #31

Given premises:
Ultimate epistemic interests:
     (p <-> p)    interest = 1.0

Problem #32

Given premises:
Ultimate epistemic interests:
     (((p <-> q) <-> r) <-> (p <-> (q <-> r)))    interest = 1.0

Problem #33

Given premises:
Ultimate epistemic interests:
     ((p v (q & r)) <-> ((p v q) & (p v r)))    interest = 1.0

Problem #34

Given premises:
Ultimate epistemic interests:
     ((p <-> q) <-> ((q v ~p) & (~q v p)))    interest = 1.0

Problem #35

Given premises:
Ultimate epistemic interests:
     ((p <-> q) -> (~p v q))    interest = 1.0

Problem #36

Given premises:
Ultimate epistemic interests:
     ((p -> q) v (q -> p))    interest = 1.0

Problem #37

Given premises:
Ultimate epistemic interests:
     (((p & (q -> r)) -> s) <-> ((~p v (q v s)) & (~p v (~r v s))))    interest = 1.0

Problem #41
Given premises:
    (all x)(F x)    justification = 1.0

Ultimate epistemic interests:
    (some x)(F x)    interest = 1.0

Problem #42
Given premises:
    (some x)(all y)(F x y)    justification = 1.0

Ultimate epistemic interests:
    (all y)(some x)(F x y)    interest = 1.0

Problem #43
Given premises:
    (all x)((P x) -> ~(P x))    justification = 1.0

Ultimate epistemic interests:
    ~(P a)    interest = 1.0

Problem #44
Given premises:
    (all x)[(F x) -> ((H x) & ~(G x))]    justification = 1.0

Ultimate epistemic interests:
    ((G a) -> ~(F a))    interest = 1.0

Problem #45
Given premises:
    (all x)((H x) -> (G x))    justification = 1.0

Ultimate epistemic interests:
    [((H a) -> (G a)) & ~(~(G b) & (H b))]    interest = 1.0

Problem #46
Given premises:
    (all x)[(P x) <-> ((H x) & ~(P x))]    justification = 1.0

Ultimate epistemic interests:
    (all x)~(H x)    interest = 1.0

Problem #47
Given premises:
    (all x)(F x)    justification = 1.0
    (all x)((F x) -> (G x))    justification = 1.0

Ultimate epistemic interests:
    (all x)(G x)    interest = 1.0

Problem #48
Given premises:
    (F a)    justification = 1.0

Ultimate epistemic interests:
    (some x)((F x) v (G x))    interest = 1.0

Problem #49
Given premises:
    (some x)(F x)    justification = 1.0

Ultimate epistemic interests:
    (some x)((F x) v (G x))    interest = 1.0

Problem #50
Given premises:
    (some x)((F x) v (G x))    justification = 1.0
    ~(some x)(F x)    justification = 1.0

Ultimate epistemic interests:
    (some x)(G x)    interest = 1.0

Problem #51
Given premises:
    [(some x)(F x) -> (all y)(G y)]    justification = 1.0

Ultimate epistemic interests:
    (all x)(all y)[(F x) -> (G y)]    interest = 1.0

Problem #52
Given premises:
    (all x)[(F x) -> ((G x) -> (H x))]    justification = 1.0

Ultimate epistemic interests:
    [(all x)((F x) -> (G x)) -> (all x)((F x) -> (H x))]    interest = 1.0

Problem #53
Given premises:
    (all x)[(F x) -> (some y)((F y) & (G x y))]    justification = 1.0

Ultimate epistemic interests:
    (all x)[(F x) -> (some y)(some z)((G x y) & (G y z))]    interest = 1.0

Problem #54
Given premises:
    (all x)(some y)(R x y)    justification = 1.0
    (all x)(all y)((R x y) -> (R y x))    justification = 1.0
    (all x)(all y)(all z)([(R x y) & (R y z)] -> (R x z))    justification = 1.0

Ultimate epistemic interests:
    (all x)(R x x)    interest = 1.0

Problem #55
Given premises:

Ultimate epistemic interests:
    [(all x)(F x) -> (some x)(F x)]    interest = 1.0

Problem #56
Given premises:

Ultimate epistemic interests:
    (some x)[(F x) -> (all y)(F y)]    interest = 1.0

Problem #57
Given premises:

Ultimate epistemic interests:
    [(all x)(all y)((R x y) -> ~(R y x)) -> ~(some x)(R x x)]    interest = 1.0

Problem #58
Given premises:

Ultimate epistemic interests:
    ~(some x)(all y)((R x y) <-> ~(R y y))    interest = 1.0

Problem #59
Given premises:

Ultimate epistemic interests:
    ~(all x)[((F x) v ~(F x)) -> ~((F x) v ~(F x))]    interest = 1.0

Problem #60
Given premises:

Ultimate epistemic interests:
    [(some x)((F x) v (G x)) <-> [(some x)(F x) v (some x)(G x)]]    interest = 1.0

Problem #61
Given premises:

Ultimate epistemic interests:
    [(all x)((F x) & (G x)) <-> [(all x)(F x) & (all x)(G x)]]    interest = 1.0

Problem #62
Given premises:

Ultimate epistemic interests:
    [(all x)((F x) -> (G x)) -> ((all x)(F x) -> (all x)(G x))]    interest = 1.0

Problem #63
Given premises:

Ultimate epistemic interests:
    [(P -> (all x)(F x)) <-> (all x)(P -> (F x))]    interest = 1.0

Problem #64
Given premises:

Ultimate epistemic interests:
    [(P -> (some x)(F x)) <-> (some x)(P -> (F x))]    interest = 1.0

Problem #65
Given premises:

Ultimate epistemic interests:
    [((all x)(F x) -> P) <-> (some x)((F x) -> P)]    interest = 1.0

Problem #66
Given premises:

Ultimate epistemic interests:
    (all x)((F x) v ~(F x))    interest = 1.0

Problem #67
Given premises:

Ultimate epistemic interests:
    (some x)((F x) v ~(F x))    interest = 1.0

Problem #68
Given premises:

Ultimate epistemic interests:
    (some y)((F a y) <-> (F y y))    interest = 1.0

Problem #69
Given premises:

Ultimate epistemic interests:
    (all x)(some y)((F x y) <-> (F y y))    interest = 1.0

Problem #70
     Pelletier's problem 18
Given premises:

Ultimate epistemic interests:
    (some y)(all x)((F y) -> (F x))    interest = 1.0

Problem #71
     Pelletier's problem 19
Given premises:

Ultimate epistemic interests:
    (some x)(all y)(all z)(((P y) -> (Q z)) -> ((P x) -> (Q x)))    interest = 1.0

Problem #72
     Pelletier's problem 20
Given premises:

Ultimate epistemic interests:
    [(all x)(all y)(some z)(all w)(((P x) & (Q y)) -> ((R z) & (S w)))
                  -> ((some v1)(some u)((P v1) & (Q u)) -> (some s)(R s))]    interest = 1.0

Problem #73
     Pelletier's problem 21
Given premises:
    (some x)(p -> (F x))    justification = 1.0
    (some x)((F x) -> p)    justification = 1.0

Ultimate epistemic interests:
    (some x)(p <-> (F x))    interest = 1.0

Problem #74
     Pelletier's problem 22
Given premises:

Ultimate epistemic interests:
    [(all x)(p <-> (F x)) -> (p <-> (all y)(F y))]    interest = 1.0

Problem #75
     Pelletier's problem 23
Given premises:

Ultimate epistemic interests:
    [(all x)(p v (F x)) <-> (p v (all y)(F y))]    interest = 1.0

Problem #76
     Pelletier's problem 24
Given premises:
    ~(some x)((S x) & (Q x))    justification = 1.0
    (all x)((P x) -> ((Q x) v (R x)))    justification = 1.0
    [~(some x)(P x) -> (some y)(Q y)]    justification = 1.0
    (all x)(((Q x) v (R x)) -> (S x))    justification = 1.0

Ultimate epistemic interests:
    (some x)((P x) & (R x))    interest = 1.0

Problem #77
     Pelletier's problem 25
Given premises:
    (some x)(P x)    justification = 1.0
    (all x)((F x) -> (~(G x) & (R x)))    justification = 1.0
    (all x)((P x) -> ((G x) & (F x)))    justification = 1.0
    [(all x)((P x) -> (Q x)) v (some y)((P y) & (R y))]    justification = 1.0

Ultimate epistemic interests:
    (some x)((Q x) & (P x))    interest = 1.0

Problem #78
     Pelletier's problem 26
Given premises:
    [(some x)(P x) <-> (some y)(Q y)]    justification = 1.0
    (all x)(all y)(((P x) & (Q y)) -> ((R x) <-> (S y)))    justification = 1.0

Ultimate epistemic interests:
    [(all x)((P x) -> (R x)) <-> (all y)((Q y) -> (S y))]    interest = 1.0

Problem #79
     Pelletier's problem 27
Given premises:
    (some x)((F x) & ~(G x))    justification = 1.0
    (all x)((F x) -> (H x))    justification = 1.0
    (all x)(((J x) & (I x)) -> (F x))    justification = 1.0
    [(some x)((H x) & ~(G x)) -> (all y)((I y) -> ~(H y))]    justification = 1.0

Ultimate epistemic interests:
    (all x)((J x) -> ~(I x))    interest = 1.0

Problem #80
     Pelletier's problem 28
Given premises:
    (all x)[(P x) -> (all x)(Q x)]    justification = 1.0
    [(all x)((Q x) v (R x)) -> (some y)((Q y) & (S y))]    justification = 1.0
    [(some x)(S x) -> (all x)((F x) -> (G x))]    justification = 1.0

Ultimate epistemic interests:
    (all x)[((P x) & (F x)) -> (G x)]    interest = 1.0

Problem #81
     Pelletier's problem 29
Given premises:
    [(some x)(F x) & (some y)(G y)]    justification = 1.0

Ultimate epistemic interests:
    ([(all x)((F x) -> (H x)) & (all y)((G y) -> (J y))] <->
          (all z)(all w)(((F z) & (G w)) -> ((H z) & (J w))))    interest = 1.0

Problem #82
     Pelletier's problem 30
Given premises:
    (all x)(((F x) v (G x)) -> ~(H x))    justification = 1.0
    (all x)(((G x) -> ~(I x)) -> ((F x) & (H x)))    justification = 1.0

Ultimate epistemic interests:
    (all x)(I x)    interest = 1.0

Problem #83
     Pelletier's problem 31
Given premises:
    ~(some x)((F x) & ((G x) v (H x)))    justification = 1.0
    (some x)((I x) & (F x))    justification = 1.0
    (all x)(~(H x) -> (J x))    justification = 1.0

Ultimate epistemic interests:
    (some x)((I x) & (J x))    interest = 1.0

Problem #84
     Pelletier's problem 32
Given premises:
    (all x)(((F x) & ((G x) v (H x))) -> (I x))    justification = 1.0
    (all x)(((I x) & (H x)) -> (J x))    justification = 1.0
    (all x)((K x) -> (H x))    justification = 1.0

Ultimate epistemic interests:
    (all x)(((F x) & (K x)) -> (J x))    interest = 1.0

Problem #85
     Pelletier's problem 33
Given premises:

Ultimate epistemic interests:
    [(all x)[((P a) & ((P x) -> (P b))) -> (P c)] <->
                  (all x)((~(P a) v ((P x) v (P c))) & (~(P a) v (~(P b) v (P c))))]    interest = 1.0

Problem #86
     Half of Pelletier's problem 34
Given premises:

Ultimate epistemic interests:
    [[(some x)(all y)((P x) <-> (P y)) <-> ((some z)(Q z) <-> (all w)(Q w))] ->
              [(some u)(all v1)((Q u) <-> (Q v1)) <-> ((some r)(P r) <-> (all s)(P s))]]    interest = 1.0

Problem #87
     Pelletier's problem 35
Given premises:

Ultimate epistemic interests:
    (some u)(some v1)[(P u v1) -> (all x)(all y)(P x y)]    interest = 1.0

Problem #88
     Pelletier's problem 36
Given premises:
    (all x)(some y)(F x y)    justification = 1.0
    (all x)(some z)(G x z)    justification = 1.0
    (all x)(all y)[((F x y) v (G x y)) -> (all z)(((F y z) v (G y z)) -> (H x z))]    justification = 1.0

Ultimate epistemic interests:
    (all x)(some y)(H x y)    interest = 1.0

Problem #89
     Pelletier's problem 37
Given premises:
    (all z)(some w)(all x)(some y)[[((P x z) -> (P y w)) & (P y z)] &
               [(P y w) -> (some u)(Q u w)]]    justification = 1.0
    (all x)(all z)[~(P x z) -> (some v1)(Q v1 z)]    justification = 1.0
    [(some y)(some s)(Q y s) -> (all x)(R x x)]    justification = 1.0

Ultimate epistemic interests:
    (all x)(some y)(R x y)    interest = 1.0

Problem #90
     Pelletier's problem 38
Given premises:

Ultimate epistemic interests:
    [(all x)[[(P a) & ((P x) -> (some y)((P y) & (R x y)))] ->
                  (some z)(some w)[(P z) & ((R x w) & (R w z))]] <->
                     (all x)[[(~(P a) v (P x)) v (some z)(some w)((P z) & ((R x w) & (R w z)))] & 
                    [~(P a) v (~(some y)((P y) & (R x y)) v
                     (some z)(some w)((P z) & ((R x w) & (R w z))))]]]    interest = 1.0

Problem #91
     Pelletier's problem 39
Given premises:

Ultimate epistemic interests:
    ~(some x)(all y)((F y x) <-> ~(F y y))    interest = 1.0

Problem #92
     Pelletier's problem 40
Given premises:

Ultimate epistemic interests:
    [(some y)(all x)((F x y) <-> (F x x)) -> ~(all z)(some w)(all v1)((F v1 w) <-> ~(F v1 z))]    interest = 1.0

Problem #93
     Pelletier's problem 41
Given premises:
    (all z)(some y)(all x)[(F x y) <-> ((F x z) & ~(F x x))]    justification = 1.0

Ultimate epistemic interests:
    ~(some z)(all x)(F x z)    interest = 1.0

Problem #94
     Pelletier's problem 42
Given premises:

Ultimate epistemic interests:
    ~(some y)(all x)[(F x y) <-> ~(some z)((F x z) & (F z x))]    interest = 1.0

Problem #95
     Pelletier's problem 43
Given premises:
    (all x)(all y)[(Q x y) <-> (all z)((F z x) <-> (F z y))]    justification = 1.0

Ultimate epistemic interests:
    (all x)(all y)[(Q x y) <-> (Q y x)]    interest = 1.0

Problem #96
     Pelletier's problem 44
Given premises:
    (all x)[[(F x) -> (some y)((G y) & (H x y))] & (some y)((G y) & ~(H x y))]    justification = 1.0
    (some x)[(J x) & (all y)[(G y) -> (H x y)]]    justification = 1.0

Ultimate epistemic interests:
    (some x)((J x) & ~(F x))    interest = 1.0

Problem #97
     Pelletier's problem 45
Given premises:
    (all x)[[(F x) & (all y)[((G y) & (H x y)) -> (J x y)]] ->
                (all y)[((G y) & (H x y)) -> (K y)]]    justification = 1.0
    ~(some y)((L y) & (K y))    justification = 1.0
    (some x)[[(F x) & (all y)((H x y) -> (L y))] &
             (all y)(((G y) & (H x y)) -> (J x y))]    justification = 1.0

Ultimate epistemic interests:
    (some x)((F x) & ~(some y)((G y) & (H x y)))    interest = 1.0

Problem #98
     Pelletier's problem 46
Given premises:
    (all x)([(F x) & (all y)[((F y) & (H y x)) -> (G y)]] -> (G x))    justification = 1.0
    [(some x)((F x) & ~(G x)) ->
             (some x)(((F x) & ~(G x)) & (all y)(((F y) & ~(G y)) -> (J x y)))]    justification = 1.0
    (all x)(all y)[[((F x) & (F y)) & (H x y)] -> ~(J y x)]    justification = 1.0

Ultimate epistemic interests:
    (all x)((F x) -> (G x))    interest = 1.0

Problem #99
     Pelletier's problem 47
Given premises:
    (all x)((W x) -> (A x))    justification = 1.0
    (all x)((F x) -> (A x))    justification = 1.0
    (all x)((B x) -> (A x))    justification = 1.0
    (all x)((C x) -> (A x))    justification = 1.0
    (all x)((S x) -> (A x))    justification = 1.0
    (some w0)(W w0)    justification = 1.0
    (some f0)(F f0)    justification = 1.0
    (some b0)(B b0)    justification = 1.0
    (some c0)(C c0)    justification = 1.0
    (some s0)(S s0)    justification = 1.0
    (some g0)(G g0)    justification = 1.0
    (all x)((G x) -> (P x))    justification = 1.0
    (all x)[(A x) -> [(all w)((P w) -> (E x w)) v
             (all y)(((A y) & ((M y x) & (some z)((P z) & (E y z)))) -> (E x y))]]    justification = 1.0
    (all x)(all y)[((C x) & (B y)) -> (M x y)]    justification = 1.0
    (all x)(all y)[((S x) & (B y)) -> (M x y)]    justification = 1.0
    (all x)(all y)[((B x) & (F y)) -> (M x y)]    justification = 1.0
    (all x)(all y)[((F x) & (W y)) -> (M x y)]    justification = 1.0
    (all x)(all y)[((W x) & (F y)) -> ~(E x y)]    justification = 1.0
    (all x)(all y)[((W x) & (G y)) -> ~(E x y)]    justification = 1.0
    (all x)(all y)[((B x) & (C y)) -> (E x y)]    justification = 1.0
    (all x)(all y)[((B x) & (S y)) -> ~(E x y)]    justification = 1.0
    (all x)[(C x) -> (some y)((P y) & (E x y))]    justification = 1.0
    (all x)[(S x) -> (some y)((P y) & (E x y))]    justification = 1.0

Ultimate epistemic interests:
    (some x)(some y)[[(A x) & (A y)] & (some z)[(E x y) & ((G z) & (E y z))]]    interest = 1.0

Problem #100
     Pelletier's problem 57
Given premises:
    (F (g a b) (g b c))    justification = 1.0
    (F (g b c) (g a c))    justification = 1.0
    (all x)(all y)(all z)[[(F x y) & (F y z)] -> (F x z)]    justification = 1.0

Ultimate epistemic interests:
    (F (g a b) (g a c))    interest = 1.0

Problem #102
Given premises:

Ultimate epistemic interests:
    [(all x)[((F a) & ((F x) -> (F (g x)))) -> (F (g (g x)))] ->
          (all x)[[(~(F a) v (F x)) v (F (g (g x)))] &
               [(~(F a) v ~(F (g x))) v (F (g (g x)))]]]    interest = 1.0

Problem #103
     The unintuitive problem
Given premises:
    (all x)(all y)(all z)([(P x y) & (P y z)] -> (P x z))    justification = 1.0
    (all x)(all y)(all z)([(Q x y) & (Q y z)] -> (Q x z))    justification = 1.0
    (all x)(all y)((Q x y) -> (Q y x))    justification = 1.0
    (all x)(all y)(~(P x y) -> (Q x y))    justification = 1.0
    ~(P a b)    justification = 1.0

Ultimate epistemic interests:
    (Q c d)    interest = 1.0

Problem #104
     Chang and Lee problem 3
Given premises:
    (all x)(P x e x)    justification = 1.0
    (all x)(P e x x)    justification = 1.0
    (all x)(all y)(all z)(all u)(all v1)(all w)[((P x y u) & ((P y z v1) & (P u z w))) -> (P x v1 w)]    justification = 1.0
    (all x)(all y)(all z)(all u)(all v1)(all w)[((P x y u) & ((P y z v1) & (P x v1 w))) -> (P u z w)]    justification = 1.0
    (all x)(P x x e)    justification = 1.0
    (P a b c)    justification = 1.0

Ultimate epistemic interests:
    (P b a c)    interest = 1.0
               |#
"
))
)

(defunction test* () (test :skip 86))