Logicproof Package and Axiomatic proof, issues with Layout

Here is how you could redefine the logicproof environment ot allow linebreaks in the second column. (If the length of the text in the last column and/or the textwidth are changes, the width of the second column should be adjusted. Unfortunately I couldn't get tabularx to work properly here.)

documentclass[12pt,a4paper,oneside, onehalfspacing openright]{book}
usepackage{logicproof}
usepackage{amsmath, amsthm, amssymb, amsfonts}

makeatletter
renewenvironment{logicproof}[1]{%
  setcounter{lp@line}{0}%
  setcounter{lp@nested}{0}%
  setcounter{lp@total@nests}{#1}%
  setlength{tabcolsep}{0mm}%
  letlp@orig@arraycr@arraycr%
  renewcommand{@arraycr}{lp@cr}%
  renewcommand{@currentlabel}{p@lp@linethelp@line}%
  ifthenelse{%
    0=#1%
  }{%
    deflp@tab@format{{r@{~~~}>{raggedrightarraybackslash(displaystyle}p{9cm}<{)}@{~~~~}l}}%
  }{%
    deflp@tab@format%
        {{r@{~~~}*{#1}{l}@{~}>{raggedrightarraybackslash(displaystyle}p{9cm}<{)}@{~~~~}l@{~}*{#1}{r}}}
  }%
  center%
  expandaftertabularlp@tab@format%
  lp@start@proof@line%
}{%
  lp@stop@proof@line%
  endtabular%
  endcenter%
  setcounter{lp@total@nests}{0}%
  ifthenelse{%
    0=value{lp@nested}
  }{% All is well.
  }{% There are still open subproofs.
    def@currenvir{subproof}%
  }
}
makeatother

begin{document}
begin{logicproof}{0}
    vdash textbf{I} (overline{textbf{K1} land textbf{K2} land textbf{K3} land dagger^{*}, neg V3}) & from $spadesuit$
    textbf{K2} vdash textbf{K} (overline{textbf{K1} land textbf{K2} land textbf{K3}}) & instance of textbf{K2}
    dagger^{**} vdash textbf{K}(overline{dagger^{*}}) & $dagger^{**}$
    textbf{K3} vdash  textbf{I} (overline{textbf{K1} land textbf{K2} land textbf{K3} land dagger^{*}, neg V3}) land  textbf{K}_{s} (overline{textbf{K1} land textbf{K2} land textbf{K3}}) land textbf{K}_{s}(overline{dagger^{*}}) rightarrow textbf{K}_{s} (overline{neg V3})& intance of textbf{K3}
    textbf{K2, K3}, dagger^{**} vdash textbf{K}_{s} (overline{neg V3}) & MP from 1, 2, 3, 4
    vdash  textbf{K}_{s} (overline{neg V3}) rightarrow V3 &logic from V3
    textbf{K2, K3}, dagger^{**} vdash V3 &  MP from 5, 6
    textbf{K1, K2, K3}, dagger^{*}, dagger^{**} vdash  V3 land neg V3 & from 7 and $spadesuit$
end{logicproof}    
end{document}