Goal

J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- Jm3

Linearized Gentzen Proof

  1. m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by Axiom
  2. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; ~m3 by =>not
  3. m2; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by Axiom
  4. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; ~m2 by =>not
  5. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; (~m2 & ~m3) by =>&
  6. m1; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by Axiom
  7. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; ~m1 by =>not
  8. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; (~m1 & (~m2 & ~m3)) by =>&
  9. ~(~m1 & (~m2 & ~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by not=>
  10. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by []=>
  11. ~m2; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m3 by not=>
  12. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m3 by []=>
  13. ~m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1 by not=>
  14. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1 by []=>
  15. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3; K2~m3 >- m2; m3; K1m1; K1~m1 by =>[1]
  16. m3; ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3; K1~m2; K2~m3 >- m2; m3; K1m1; K1~m1 by Axiom
  17. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3; K1~m2; K2~m3 >- m2; m3; K1m1; K1~m1 by []=>
  18. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K2~m3 >- m2; m3; K1m1; K1~m1 by or=>
  19. m2; ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m2; K2~m3 >- m2; m3; K1m1; K1~m1 by Axiom
  20. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m2; K2~m3 >- m2; m3; K1m1; K1~m1 by []=>
  21. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3; K1m1; K1~m1 by or=>
  22. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3; (K1m1 ∨ K1~m1) by =>or
  23. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); ~(K1m1 ∨ K1~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by not=>
  24. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by []=>
  25. ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))); (K1m2 ∨ K1~m2); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by &=>
  26. ((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by &=>
  27. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by []=>
  28. ~m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2 by not=>
  29. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2 by []=>
  30. (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3; K2~m3 >- m3; K2m2; K2~m2 by =>[2]
  31. m3; (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3; K2m3 >- m3; K2m2; K2~m2 by Axiom
  32. (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3; K2m3 >- m3; K2m2; K2~m2 by []=>
  33. (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3 >- m3; K2m2; K2~m2 by or=>
  34. (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); ~m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3 >- m3; K2m2; K2~m2 by not=>
  35. (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3 >- m3; K2m2; K2~m2 by []=>
  36. m3; (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3 >- m3; K2m2; K2~m2 by Axiom
  37. (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3 >- m3; K2m2; K2~m2 by []=>
  38. (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by or=>
  39. ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by &=>
  40. ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))); (K1m2 ∨ K1~m2); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by &=>
  41. ((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by &=>
  42. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by []=>
  43. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; (K2m2 ∨ K2~m2) by =>or
  44. ~(K2m2 ∨ K2~m2); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3 by not=>
  45. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3 by []=>
  46. J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- Jm3 by =>[0]

Complexity

Actual Gentzen proof: 40 rules, root sequent size 57, total length 3439

Number of rules and external term size should be O(1600..9409..11826721), the total hilbert proof length should be O(4096000000..1654219191218281803361)

Actual Hilbert proof: 1519 rules, external term size - 760, total length - 572811

Hilbert Proof

    1. 1. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V3:(~(K2m2 ∨ K2~m2)) Hyp 0
    2. 2. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V2:(~(K1m1 ∨ K1~m1)) Hyp 1
    3. 3. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V1:(~(~m1 & (~m2 & ~m3))) Hyp 2
    4. 4. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) Hyp 3
    5. 5. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 5
    6. 6. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V1:(~(~m1 & (~m2 & ~m3))) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 4 and 5
    7. 7. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) MP on 3 and 6
    8. 8. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 5
    9. 9. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V2:(~(K1m1 ∨ K1~m1)) → ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 7 and 8
    10. 10. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) MP on 2 and 9
    11. 11. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 5
    12. 12. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 10 and 11
    13. 13. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 1 and 12
    14. 14.  |- (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) 4 times Deduction
    15. 15.  |- Tt:(((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))))) CS for classical tautology or t:A->A
    16. 16.  |- (Tt:(((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))))) → ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))))) Axiom 13
    17. 17.  |- ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) MP on 15 and 16
    18. 18.  |- ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 14 and 17
    19.  |- ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5   ((C5   ((C5   !V0)   !V1))   !V2))   !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) lemma3, >1 hyps
    1. 20. K2K2~m3 |- K2K2~m3 Hyp 0
    2. 21. K2K2~m3 |- (K2~m3 → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 5
    3. 22. K2K2~m3 |- K2(K2~m3 → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Nec
    4. 23. K2K2~m3 |- (K2(K2~m3 → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → (K2K2~m3 → K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 17
    5. 24. K2K2~m3 |- (K2K2~m3 → K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 22 and 23
    6. 25. K2K2~m3 |- K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 20 and 24
    7. 26. K2K2~m3 |- (K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 17
    8. 27. K2K2~m3 |- (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 25 and 26
    9. 28.  |- (K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) 1 times Deduction
    10. 29.  |- Tt:(((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) CS for classical tautology or t:A->A
    11. 30.  |- (Tt:(((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) → ((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 13
    12. 31.  |- ((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 29 and 30
    13. 32.  |- ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 28 and 31
    14. 33.  |- Tt:((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
    15. 34.  |- (Tt:((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
    16. 35.  |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))))) MP on 33 and 34
    17. 36.  |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))) MP on 32 and 35
    18. 37. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) Hyp 0
    19. 38. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 5
    20. 39. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Nec
    21. 40. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 17
    22. 41. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 39 and 40
    23. 42. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 37 and 41
    24. 43. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 17
    25. 44. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 42 and 43
    26. 45.  |- (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) 1 times Deduction
    27. 46.  |- Tt:(((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
    28. 47.  |- (Tt:(((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
    29. 48.  |- ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 46 and 47
    30. 49.  |- ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 45 and 48
    31. 50.  |- (((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 1
    32. 51.  |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 49 and 50
    33. 52.  |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 2
    34. 53.  |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 51 and 52
    35. 54.  |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 36 and 53
    36. 55.  |- Tt:(((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
    37. 56.  |- (Tt:(((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
    38. 57.  |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))))) MP on 55 and 56
    39. 58.  |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))) MP on 54 and 57
    40. 59. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) Hyp 0
    41. 60. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 5
    42. 61. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Nec
    43. 62. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 17
    44. 63. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 61 and 62
    45. 64. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 59 and 63
    46. 65. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 17
    47. 66. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 64 and 65
    48. 67.  |- (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) 1 times Deduction
    49. 68.  |- Tt:(((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
    50. 69.  |- (Tt:(((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
    51. 70.  |- ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 68 and 69
    52. 71.  |- ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 67 and 70
    53. 72.  |- (((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 1
    54. 73.  |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 71 and 72
    55. 74.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 2
    56. 75.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 73 and 74
    57. 76.  |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 58 and 75
    58. 77.  |- Tt:((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
    59. 78.  |- (Tt:((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
    60. 79.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))))) MP on 77 and 78
    61. 80.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))) MP on 76 and 79
    62. 81. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) Hyp 0
    63. 82. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 5
    64. 83. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Nec
    65. 84. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 17
    66. 85. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 83 and 84
    67. 86. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 81 and 85
    68. 87. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 17
    69. 88. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 86 and 87
    70. 89.  |- (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) 1 times Deduction
    71. 90.  |- Tt:(((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
    72. 91.  |- (Tt:(((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
    73. 92.  |- ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 90 and 91
    74. 93.  |- ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 89 and 92
    75. 94.  |- (((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 1
    76. 95.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 93 and 94
    77. 96.  |- ((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 2
    78. 97.  |- ((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 95 and 96
    79. 98.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 80 and 97
    99.  |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) &&([] []i ai) -> []ais
    1. 100. K1K1~m2 |- K1K1~m2 Hyp 0
    2. 101. K1K1~m2 |- (K1~m2 → (K1~m3 → (K1~m2 & K1~m3))) Axiom 5
    3. 102. K1K1~m2 |- K1(K1~m2 → (K1~m3 → (K1~m2 & K1~m3))) Nec
    4. 103. K1K1~m2 |- (K1(K1~m2 → (K1~m3 → (K1~m2 & K1~m3))) → (K1K1~m2 → K1(K1~m3 → (K1~m2 & K1~m3)))) Axiom 17
    5. 104. K1K1~m2 |- (K1K1~m2 → K1(K1~m3 → (K1~m2 & K1~m3))) MP on 102 and 103
    6. 105. K1K1~m2 |- K1(K1~m3 → (K1~m2 & K1~m3)) MP on 100 and 104
    7. 106. K1K1~m2 |- (K1(K1~m3 → (K1~m2 & K1~m3)) → (K1K1~m3 → K1(K1~m2 & K1~m3))) Axiom 17
    8. 107. K1K1~m2 |- (K1K1~m3 → K1(K1~m2 & K1~m3)) MP on 105 and 106
    9. 108.  |- (K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) 1 times Deduction
    10. 109.  |- Tt:(((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)))) CS for classical tautology or t:A->A
    11. 110.  |- (Tt:(((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)))) → ((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)))) Axiom 13
    12. 111.  |- ((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3))) MP on 109 and 110
    13. 112.  |- ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) MP on 108 and 111
    14. 113.  |- Tt:((((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) CS for classical tautology or t:A->A
    15. 114.  |- (Tt:((((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) → (((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 13
    16. 115.  |- (((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 113 and 114
    17. 116.  |- (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 112 and 115
    18. 117. K1(K1~m2 & K1~m3) |- K1(K1~m2 & K1~m3) Hyp 0
    19. 118. K1(K1~m2 & K1~m3) |- ((K1~m2 & K1~m3) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 5
    20. 119. K1(K1~m2 & K1~m3) |- K1((K1~m2 & K1~m3) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Nec
    21. 120. K1(K1~m2 & K1~m3) |- (K1((K1~m2 & K1~m3) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → (K1(K1~m2 & K1~m3) → K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 17
    22. 121. K1(K1~m2 & K1~m3) |- (K1(K1~m2 & K1~m3) → K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 119 and 120
    23. 122. K1(K1~m2 & K1~m3) |- K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 117 and 121
    24. 123. K1(K1~m2 & K1~m3) |- (K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 17
    25. 124. K1(K1~m2 & K1~m3) |- (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 122 and 123
    26. 125.  |- (K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) 1 times Deduction
    27. 126.  |- Tt:(((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) CS for classical tautology or t:A->A
    28. 127.  |- (Tt:(((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) → ((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 13
    29. 128.  |- ((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 126 and 127
    30. 129.  |- ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 125 and 128
    31. 130.  |- (((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 1
    32. 131.  |- (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 129 and 130
    33. 132.  |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 2
    34. 133.  |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 131 and 132
    35. 134.  |- (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 116 and 133
    36. 135.  |- Tt:(((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
    37. 136.  |- (Tt:(((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
    38. 137.  |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))))) MP on 135 and 136
    39. 138.  |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))) MP on 134 and 137
    40. 139. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) Hyp 0
    41. 140. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 5
    42. 141. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Nec
    43. 142. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 17
    44. 143. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 141 and 142
    45. 144. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 139 and 143
    46. 145. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 17
    47. 146. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 144 and 145
    48. 147.  |- (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) 1 times Deduction
    49. 148.  |- Tt:(((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
    50. 149.  |- (Tt:(((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
    51. 150.  |- ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 148 and 149
    52. 151.  |- ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 147 and 150
    53. 152.  |- (((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 1
    54. 153.  |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 151 and 152
    55. 154.  |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 2
    56. 155.  |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 153 and 154
    57. 156.  |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 138 and 155
    58. 157.  |- Tt:((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
    59. 158.  |- (Tt:((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
    60. 159.  |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))))) MP on 157 and 158
    61. 160.  |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))) MP on 156 and 159
    62. 161. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) Hyp 0
    63. 162. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 5
    64. 163. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Nec
    65. 164. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 17
    66. 165. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 163 and 164
    67. 166. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 161 and 165
    68. 167. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 17
    69. 168. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 166 and 167
    70. 169.  |- (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) 1 times Deduction
    71. 170.  |- Tt:(((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
    72. 171.  |- (Tt:(((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
    73. 172.  |- ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 170 and 171
    74. 173.  |- ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 169 and 172
    75. 174.  |- (((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 1
    76. 175.  |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 173 and 174
    77. 176.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 2
    78. 177.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 175 and 176
    79. 178.  |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 160 and 177
    80. 179.  |- Tt:(((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
    81. 180.  |- (Tt:(((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
    82. 181.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))))) MP on 179 and 180
    83. 182.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))) MP on 178 and 181
    84. 183. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) Hyp 0
    85. 184. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 5
    86. 185. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Nec
    87. 186. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 17
    88. 187. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 185 and 186
    89. 188. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 183 and 187
    90. 189. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 17
    91. 190. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 188 and 189
    92. 191.  |- (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) 1 times Deduction
    93. 192.  |- Tt:(((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
    94. 193.  |- (Tt:(((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
    95. 194.  |- ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 192 and 193
    96. 195.  |- ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 191 and 194
    97. 196.  |- (((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 1
    98. 197.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 195 and 196
    99. 198.  |- (((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → (((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 2
    100. 199.  |- (((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 197 and 198
    101. 200.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 182 and 199
    201.  |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) &&([] []i ai) -> []ais
    1. 202.  |- Tt:((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((m1 ∨ m2) ∨ m3))) CS for classical tautology or t:A->A
    203.  |- Tt:((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((m1 ∨ m2) ∨ m3))) Axiom
    1. 204.  |- Tt:(((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((m1 ∨ m2) ∨ m3)) → ((((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → (((m1 ∨ m2) ∨ m3) ∨ ~m3)))) CS for classical tautology or t:A->A
    2. 205.  |- (Tt:(((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2