1.2
wnds:Windows 954.10
FchF
C971368126520D971368847360D971369035540D971369416340C983162038570D983162461610C983219486570D983219587420C983219660740D983219696120
newFormat
{p=proof{p{s()r{u=uProof;s=proof;}o{c=0;s="";l="";}f(t{s(i{r=fol{t="(A & ~B) | (C | D)";b()g=@;}})r{u=uPremise;s=proof;}o{c=0;s="";l="";}s()},t{s(i{r=fol{t="~C & B";b()g=@;}})r{u=uPremise;s=proof;}o{c=0;s="";l="";}s()},p{s()r{u=uProof;s=proof;}o{c=0;s="";l="";}f(t{s(i{r=fol{t="A & ~B";b()g=@;}})r{u=uPremise;s=proof;}o{c=0;s="";l="";}s()},t{s(i{r=fol{t="";b()g=@;}})r{u="uRule?";s=proof;}o{c=0;s="";l="";}s()},t{s(i{r=fol{t=D;b()g=@;}})r{u="uRule?";s=proof;}o{c=0;s="";l="";}s()})},p{s()r{u=uProof;s=proof;}o{c=0;s="";l="";}f(t{s(i{r=fol{t=C;b()g=@;}})r{u=uPremise;s=proof;}o{c=0;s="";l="";}s()},t{s(i{r=fol{t="";b()g=@;}})r{u="uRule?";s=proof;}o{c=0;s="";l="";}s()},t{s(i{r=fol{t=D;b()g=@;}})r{u="uRule?";s=proof;}o{c=0;s="";l="";}s()})},p{s()r{u=uProof;s=proof;}o{c=0;s="";l="";}f(t{s(i{r=fol{t=D;b()g=@;}})r{u=uPremise;s=proof;}o{c=0;s="";l="";}s()})},t{s(i{r=fol{t=D;b()g=@;}})r{u="u\u2228 Elim";s=fol;}o{c=0;s="";l="";}s(s=0;,s=2.;,s=3.;,s=4.;)},p{s()r{u=uProof;s=proof;}o{c=0;s="";l="";}f(t{s(i{r=fol{t="~D";b()g=@;}})r{u=uPremise;s=proof;}o{c=0;s="";l="";}s()},t{s(i{r=fol{t="^";b()g=@;}})r{u="u\u22A5 Intro";s=fol;}o{c=0;s="";l="";}s(s=5;,s=6.0;)})},t{s(i{r=fol{t="~~D";b()g=@;}})r{u="u\254 Intro";s=fol;}o{c=0;s="";l="";}s(s=6.;)})}g{g(s{g{r=fol{t="~~D";b()g=@;}}r{u=uFOLGoalRule;s=fol;}s()o{c=0;s="";l="";}})}a=true;}}c=122131;