1.2
wnds:Windows 954.10
FchF
C971368126520D971368847360D971369035540D971369416340D971369578530C971369813780D971369849260C971370578450D971370597780C983162742830D983162969170D983163068480D983163092430C983219706220D983219732810
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";b()g=@;}})r{u="u\u2227 Elim";s=fol;}o{c=0;s="";l="";}s(s=2.0;)},t{s(i{r=fol{t=B;b()g=@;}})r{u="u\u2227 Elim";s=fol;}o{c=0;s="";l="";}s(s=1;)},t{s(i{r=fol{t="^";b()g=@;}})r{u="u\u22A5 Intro";s=fol;}o{c=0;s="";l="";}s(s=2.1;,s=2.2;)},t{s(i{r=fol{t=D;b()g=@;}})r{u="u\u22A5 Elim";s=fol;}o{c=0;s="";l="";}s(s=2.3;)})},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=1;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=1;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=1;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=140356;