%! poi_theorem(?TheoremId, ?TheoremFormula, ?ProblemId, ?Rating) is nondet.
%
% Facts with the 1374 POI theorems. TheoremId comes from set.mm. ProblemId is
% the basename for the corresponding TPTP problems.
%
% If loaded into plain Prolog (in contrast to CD Tools) it needs an operator
% declaration for "=>", e.g., ":- op(1150,xfx,=>)".
%
poi_theorem(mp2, (A=>(B=>((A=>(B=>C))=>C))), poi_000001_mp2, 0.22).
poi_theorem(mp2b, (A=>((A=>B)=>((B=>C)=>C))), poi_000002_mp2b, 0).
poi_theorem('3syl', ((A=>B)=>((B=>C)=>((C=>D)=>(A=>D)))), poi_000003_3syl, 0).
poi_theorem('4syl', ((A=>B)=>((B=>C)=>((C=>D)=>((D=>E)=>(A=>E))))), poi_000004_4syl, 0.11).
poi_theorem(mpi, (A=>((B=>(A=>C))=>(B=>C))), poi_000005_mpi, 0).
poi_theorem(mpisyl, ((A=>B)=>(C=>((B=>(C=>D))=>(A=>D)))), poi_000006_mpisyl, 0.78).
poi_theorem(id, (A=>A), poi_000007_id, 0).
poi_theorem(idd, (_=>(A=>A)), poi_000008_idd, 0).
poi_theorem('2a1d', ((A=>B)=>(A=>(_=>(_=>B)))), poi_000009_2a1d, 0).
poi_theorem(a1i13, ((A=>B)=>(_=>(A=>(_=>B)))), poi_000010_a1i13, 0).
poi_theorem('2a1', (A=>(_=>(_=>A))), poi_000011_2a1, 0).
poi_theorem(a2d, ((A=>(B=>(C=>D)))=>(A=>((B=>C)=>(B=>D)))), poi_000012_a2d, 0).
poi_theorem(sylcom, ((A=>(B=>C))=>((B=>(C=>D))=>(A=>(B=>D)))), poi_000013_sylcom, 0.22).
poi_theorem(syl5com, ((A=>B)=>((C=>(B=>D))=>(A=>(C=>D)))), poi_000014_syl5com, 0).
poi_theorem(syl11, ((A=>(B=>C))=>((D=>A)=>(B=>(D=>C)))), poi_000015_syl11, 0).
poi_theorem(syl5, ((A=>B)=>((C=>(B=>D))=>(C=>(A=>D)))), poi_000016_syl5, 0).
poi_theorem(syl6, ((A=>(B=>C))=>((C=>D)=>(A=>(B=>D)))), poi_000017_syl6, 0).
poi_theorem(syl56, ((A=>B)=>((C=>(B=>D))=>((D=>E)=>(C=>(A=>E))))), poi_000018_syl56, 0.67).
poi_theorem(syl6com, ((A=>(B=>C))=>((C=>D)=>(B=>(A=>D)))), poi_000019_syl6com, 0.11).
poi_theorem(mpcom, ((A=>B)=>((B=>(A=>C))=>(A=>C))), poi_000020_mpcom, 0).
poi_theorem(syli, ((A=>(B=>C))=>((C=>(B=>D))=>(A=>(B=>D)))), poi_000021_syli, 0.33).
poi_theorem(syl2im, ((A=>B)=>((C=>D)=>((B=>(D=>E))=>(A=>(C=>E))))), poi_000022_syl2im, 0.78).
poi_theorem(syl2imc, ((A=>B)=>((C=>D)=>((B=>(D=>E))=>(C=>(A=>E))))), poi_000023_syl2imc, 0.89).
poi_theorem('pm2.27', (A=>((A=>B)=>B)), 'poi_000024_pm2.27', 0).
poi_theorem(mpdd, ((A=>(B=>C))=>((A=>(B=>(C=>D)))=>(A=>(B=>D)))), poi_000025_mpdd, 0.22).
poi_theorem(mpid, ((A=>B)=>((A=>(C=>(B=>D)))=>(A=>(C=>D)))), poi_000026_mpid, 0.22).
poi_theorem(mpdi, ((A=>B)=>((C=>(A=>(B=>D)))=>(C=>(A=>D)))), poi_000027_mpdi, 0.22).
poi_theorem(mpii, (A=>((B=>(C=>(A=>D)))=>(B=>(C=>D)))), poi_000028_mpii, 0.22).
poi_theorem(syldc, ((A=>(B=>C))=>((A=>(C=>D))=>(B=>(A=>D)))), poi_000029_syldc, 0.78).
poi_theorem(mp2d, ((A=>B)=>((A=>C)=>((A=>(B=>(C=>D)))=>(A=>D)))), poi_000030_mp2d, 0.67).
poi_theorem(a1dd, ((A=>(B=>C))=>(A=>(B=>(_=>C)))), poi_000031_a1dd, 0).
poi_theorem('2a1dd', ((A=>(B=>C))=>(A=>(B=>(_=>(_=>C))))), poi_000032_2a1dd, 0).
poi_theorem('pm2.43d', ((A=>(B=>(B=>C)))=>(A=>(B=>C))), 'poi_000033_pm2.43d', 0).
poi_theorem('pm2.43a', ((A=>(B=>(A=>C)))=>(A=>(B=>C))), 'poi_000034_pm2.43a', 0).
poi_theorem('pm2.43', ((A=>(A=>B))=>(A=>B)), 'poi_000035_pm2.43', 0).
poi_theorem(imim2d, ((A=>(B=>C))=>(A=>((D=>B)=>(D=>C)))), poi_000036_imim2d, 0).
poi_theorem(imim2, ((A=>B)=>((C=>A)=>(C=>B))), poi_000037_imim2, 0).
poi_theorem(embantd, ((A=>B)=>((A=>(C=>D))=>(A=>((B=>C)=>D)))), poi_000038_embantd, 0.56).
poi_theorem('3syld', ((A=>(B=>C))=>((A=>(C=>D))=>((A=>(D=>E))=>(A=>(B=>E))))), poi_000039_3syld, 0.89).
poi_theorem(sylsyld, ((A=>B)=>((A=>(C=>D))=>((B=>(D=>E))=>(A=>(C=>E))))), poi_000040_sylsyld, 0.67).
poi_theorem(imim3i, ((A=>(B=>C))=>((D=>A)=>((D=>B)=>(D=>C)))), poi_000041_imim3i, 0).
poi_theorem(sylc, ((A=>B)=>((A=>C)=>((B=>(C=>D))=>(A=>D)))), poi_000042_sylc, 0.78).
poi_theorem(syl3c, ((A=>B)=>((A=>C)=>((A=>D)=>((B=>(C=>(D=>E)))=>(A=>E))))), poi_000043_syl3c, 0.67).
poi_theorem(syl6mpi, ((A=>(B=>C))=>(D=>((C=>(D=>E))=>(A=>(B=>E))))), poi_000044_syl6mpi, 0.67).
poi_theorem(mpsyl, (A=>((B=>C)=>((A=>(C=>D))=>(B=>D)))), poi_000045_mpsyl, 0.67).
poi_theorem(mpsylsyld, (A=>((B=>(C=>D))=>((A=>(D=>E))=>(B=>(C=>E))))), poi_000046_mpsylsyld, 0.78).
poi_theorem(syl6c, ((A=>(B=>C))=>((A=>(B=>D))=>((C=>(D=>E))=>(A=>(B=>E))))), poi_000047_syl6c, 0.78).
poi_theorem(syl6ci, ((A=>(B=>C))=>((A=>D)=>((C=>(D=>E))=>(A=>(B=>E))))), poi_000048_syl6ci, 0.67).
poi_theorem(syldd, ((A=>(B=>(C=>D)))=>((A=>(B=>(D=>E)))=>(A=>(B=>(C=>E))))), poi_000049_syldd, 0.56).
poi_theorem(syl5d, ((A=>(B=>C))=>((A=>(D=>(C=>E)))=>(A=>(D=>(B=>E))))), poi_000050_syl5d, 0.56).
poi_theorem(syl7, ((A=>B)=>((C=>(D=>(B=>E)))=>(C=>(D=>(A=>E))))), poi_000051_syl7, 0.44).
poi_theorem(syl6d, ((A=>(B=>(C=>D)))=>((A=>(D=>E))=>(A=>(B=>(C=>E))))), poi_000052_syl6d, 0.56).
poi_theorem(syl8, ((A=>(B=>(C=>D)))=>((D=>E)=>(A=>(B=>(C=>E))))), poi_000053_syl8, 0.67).
poi_theorem(syl9, ((A=>(B=>C))=>((D=>(C=>E))=>(A=>(D=>(B=>E))))), poi_000054_syl9, 0.67).
poi_theorem(syl9r, ((A=>(B=>C))=>((D=>(C=>E))=>(D=>(A=>(B=>E))))), poi_000055_syl9r, 0.22).
poi_theorem(syl10, ((A=>(B=>C))=>((A=>(B=>(D=>E)))=>((C=>(E=>F))=>(A=>(B=>(D=>F)))))), poi_000056_syl10, 0.78).
poi_theorem(a1ddd, ((A=>(B=>(C=>D)))=>(A=>(B=>(C=>(_=>D))))), poi_000057_a1ddd, 0).
poi_theorem(imim12d, ((A=>(B=>C))=>((A=>(D=>E))=>(A=>((C=>D)=>(B=>E))))), poi_000058_imim12d, 0.67).
poi_theorem(imim1d, ((A=>(B=>C))=>(A=>((C=>D)=>(B=>D)))), poi_000059_imim1d, 0).
poi_theorem(imim1, ((A=>B)=>((B=>C)=>(A=>C))), poi_000060_imim1, 0).
poi_theorem('pm2.83', ((A=>(B=>C))=>((A=>(C=>D))=>(A=>(B=>D)))), 'poi_000061_pm2.83', 0.44).
poi_theorem(peirceroll, ((((A=>B)=>A)=>A)=>(((A=>B)=>C)=>((C=>A)=>A))), poi_000062_peirceroll, 0).
poi_theorem(com23, ((A=>(B=>(C=>D)))=>(A=>(C=>(B=>D)))), poi_000063_com23, 0).
poi_theorem(com3r, ((A=>(B=>(C=>D)))=>(C=>(A=>(B=>D)))), poi_000064_com3r, 0.44).
poi_theorem(com13, ((A=>(B=>(C=>D)))=>(C=>(B=>(A=>D)))), poi_000065_com13, 0.33).
poi_theorem(com3l, ((A=>(B=>(C=>D)))=>(B=>(C=>(A=>D)))), poi_000066_com3l, 0.11).
poi_theorem('pm2.04', ((A=>(B=>C))=>(B=>(A=>C))), 'poi_000067_pm2.04', 0).
poi_theorem(com34, ((A=>(B=>(C=>(D=>E))))=>(A=>(B=>(D=>(C=>E))))), poi_000068_com34, 0.22).
poi_theorem(com4l, ((A=>(B=>(C=>(D=>E))))=>(B=>(C=>(D=>(A=>E))))), poi_000069_com4l, 0.78).
poi_theorem(com4t, ((A=>(B=>(C=>(D=>E))))=>(C=>(D=>(A=>(B=>E))))), poi_000070_com4t, 0.78).
poi_theorem(com4r, ((A=>(B=>(C=>(D=>E))))=>(D=>(A=>(B=>(C=>E))))), poi_000071_com4r, 0.67).
poi_theorem(com24, ((A=>(B=>(C=>(D=>E))))=>(A=>(D=>(C=>(B=>E))))), poi_000072_com24, 0.56).
poi_theorem(com14, ((A=>(B=>(C=>(D=>E))))=>(D=>(B=>(C=>(A=>E))))), poi_000073_com14, 0.67).
poi_theorem(com45, ((A=>(B=>(C=>(D=>(E=>F)))))=>(A=>(B=>(C=>(E=>(D=>F)))))), poi_000074_com45, 0).
poi_theorem(com35, ((A=>(B=>(C=>(D=>(E=>F)))))=>(A=>(B=>(E=>(D=>(C=>F)))))), poi_000075_com35, 0.67).
poi_theorem(com25, ((A=>(B=>(C=>(D=>(E=>F)))))=>(A=>(E=>(C=>(D=>(B=>F)))))), poi_000076_com25, 0.78).
poi_theorem(com5l, ((A=>(B=>(C=>(D=>(E=>F)))))=>(B=>(C=>(D=>(E=>(A=>F)))))), poi_000077_com5l, 0.78).
poi_theorem(com15, ((A=>(B=>(C=>(D=>(E=>F)))))=>(E=>(B=>(C=>(D=>(A=>F)))))), poi_000078_com15, 0.78).
poi_theorem(com52l, ((A=>(B=>(C=>(D=>(E=>F)))))=>(C=>(D=>(E=>(A=>(B=>F)))))), poi_000079_com52l, 0.78).
poi_theorem(com52r, ((A=>(B=>(C=>(D=>(E=>F)))))=>(D=>(E=>(A=>(B=>(C=>F)))))), poi_000080_com52r, 0.78).
poi_theorem(com5r, ((A=>(B=>(C=>(D=>(E=>F)))))=>(E=>(A=>(B=>(C=>(D=>F)))))), poi_000081_com5r, 0.78).
poi_theorem(imim12, ((A=>B)=>((C=>D)=>((B=>C)=>(A=>D)))), poi_000082_imim12, 0.33).
poi_theorem(jarr, (((_=>A)=>B)=>(A=>B)), poi_000083_jarr, 0).
poi_theorem('pm2.86d', ((A=>((B=>C)=>(B=>D)))=>(A=>(B=>(C=>D)))), 'poi_000084_pm2.86d', 0.33).
poi_theorem('pm2.86', (((A=>B)=>(A=>C))=>(A=>(B=>C))), 'poi_000085_pm2.86', 0.11).
poi_theorem(loolin, (((A=>B)=>(B=>A))=>(B=>A)), poi_000086_loolin, 0).
poi_theorem(loowoz, (((A=>B)=>(A=>C))=>((B=>A)=>(B=>C))), poi_000087_loowoz, 0).
poi_theorem(con4, ((n(A)=>n(B))=>(B=>A)), poi_000088_con4, 0).
poi_theorem(con4d, ((A=>(n(B)=>n(C)))=>(A=>(C=>B))), poi_000089_con4d, 0).
poi_theorem(mt4, (A=>((n(B)=>n(A))=>B)), poi_000090_mt4, 0).
poi_theorem(mt4d, ((A=>B)=>((A=>(n(C)=>n(B)))=>(A=>C))), poi_000091_mt4d, 0.22).
poi_theorem(mt4i, (A=>((B=>(n(C)=>n(A)))=>(B=>C))), poi_000092_mt4i, 0.22).
poi_theorem('pm2.21d', ((A=>n(B))=>(A=>(B=>_))), 'poi_000093_pm2.21d', 0).
poi_theorem('pm2.21ddALT', ((A=>B)=>((A=>n(B))=>(A=>_))), 'poi_000094_pm2.21ddALT', 0).
poi_theorem('pm2.21', (n(A)=>(A=>_)), 'poi_000095_pm2.21', 0).
poi_theorem('pm2.24', (A=>(n(A)=>_)), 'poi_000096_pm2.24', 0).
poi_theorem(jarl, (((A=>_)=>B)=>(n(A)=>B)), poi_000097_jarl, 0).
poi_theorem('pm2.18d', ((A=>(n(B)=>B))=>(A=>B)), 'poi_000098_pm2.18d', 0).
poi_theorem('pm2.18', ((n(A)=>A)=>A), 'poi_000099_pm2.18', 0).
poi_theorem(notnotr, (n(n(A))=>A), poi_000100_notnotr, 0).
poi_theorem(notnotrd, ((A=>n(n(B)))=>(A=>B)), poi_000101_notnotrd, 0).
poi_theorem(con2d, ((A=>(B=>n(C)))=>(A=>(C=>n(B)))), poi_000102_con2d, 0).
poi_theorem(con2, ((A=>n(B))=>(B=>n(A))), poi_000103_con2, 0).
poi_theorem(mt2d, ((A=>B)=>((A=>(C=>n(B)))=>(A=>n(C)))), poi_000104_mt2d, 0.33).
poi_theorem(mt2i, (A=>((B=>(C=>n(A)))=>(B=>n(C)))), poi_000105_mt2i, 0.33).
poi_theorem(nsyl3, ((A=>n(B))=>((C=>B)=>(C=>n(A)))), poi_000106_nsyl3, 0).
poi_theorem(nsyl, ((A=>n(B))=>((C=>B)=>(A=>n(C)))), poi_000107_nsyl, 0.11).
poi_theorem(nsyl2, ((A=>n(B))=>((n(C)=>B)=>(A=>C))), poi_000108_nsyl2, 0).
poi_theorem(notnot, (A=>n(n(A))), poi_000109_notnot, 0).
poi_theorem(notnotd, ((A=>B)=>(A=>n(n(B)))), poi_000110_notnotd, 0).
poi_theorem(con1d, ((A=>(n(B)=>C))=>(A=>(n(C)=>B))), poi_000111_con1d, 0).
poi_theorem(con1, ((n(A)=>B)=>(n(B)=>A)), poi_000112_con1, 0).
poi_theorem(mt3d, ((A=>n(B))=>((A=>(n(C)=>B))=>(A=>C))), poi_000113_mt3d, 0.22).
poi_theorem(mt3i, (n(A)=>((B=>(n(C)=>A))=>(B=>C))), poi_000114_mt3i, 0.22).
poi_theorem('pm2.24d', ((A=>B)=>(A=>(n(B)=>_))), 'poi_000115_pm2.24d', 0).
poi_theorem(con3d, ((A=>(B=>C))=>(A=>(n(C)=>n(B)))), poi_000116_con3d, 0).
poi_theorem(con3, ((A=>B)=>(n(B)=>n(A))), poi_000117_con3, 0).
poi_theorem(con3rr3, ((A=>(B=>C))=>(n(C)=>(A=>n(B)))), poi_000118_con3rr3, 0.11).
poi_theorem(nsyld, ((A=>(B=>n(C)))=>((A=>(D=>C))=>(A=>(B=>n(D))))), poi_000119_nsyld, 0.78).
poi_theorem(nsyli, ((A=>(B=>C))=>((D=>n(C))=>(A=>(D=>n(B))))), poi_000120_nsyli, 0.56).
poi_theorem('pm3.2im', (A=>(B=>n((A=>n(B))))), 'poi_000121_pm3.2im', 0).
poi_theorem(jcn, (A=>(n(B)=>n((A=>B)))), poi_000122_jcn, 0).
poi_theorem(jcnd, ((A=>B)=>((A=>n(C))=>(A=>n((B=>C))))), poi_000123_jcnd, 0.11).
poi_theorem(simprim, (n((_=>n(A)))=>A), poi_000124_simprim, 0).
poi_theorem(simplim, (n((A=>_))=>A), poi_000125_simplim, 0).
poi_theorem('pm2.5g', (n((A=>_))=>(n(A)=>_)), 'poi_000126_pm2.5g', 0).
poi_theorem('pm2.5', (n((A=>B))=>(n(A)=>B)), 'poi_000127_pm2.5', 0).
poi_theorem(conax1, (n((_=>A))=>n(A)), poi_000128_conax1, 0).
poi_theorem(conax1k, (n((_=>A))=>(_=>n(A))), poi_000129_conax1k, 0).
poi_theorem('pm2.51', (n((A=>B))=>(A=>n(B))), 'poi_000130_pm2.51', 0).
poi_theorem('pm2.52', (n((A=>B))=>(n(A)=>n(B))), 'poi_000131_pm2.52', 0).
poi_theorem('pm2.521g', (n((_=>A))=>(A=>_)), 'poi_000132_pm2.521g', 0).
poi_theorem('pm2.521g2', (n((A=>_))=>(_=>A)), 'poi_000133_pm2.521g2', 0).
poi_theorem('pm2.521', (n((A=>B))=>(B=>A)), 'poi_000134_pm2.521', 0).
poi_theorem(expt, ((n((A=>n(B)))=>C)=>(A=>(B=>C))), poi_000135_expt, 0).
poi_theorem(impt, ((A=>(B=>C))=>(n((A=>n(B)))=>C)), poi_000136_impt, 0.11).
poi_theorem('pm2.61d', ((A=>(B=>C))=>((A=>(n(B)=>C))=>(A=>C))), 'poi_000137_pm2.61d', 0.22).
poi_theorem('pm2.61d1', ((A=>(B=>C))=>((n(B)=>C)=>(A=>C))), 'poi_000138_pm2.61d1', 0.11).
poi_theorem('pm2.61d2', ((A=>(n(B)=>C))=>((B=>C)=>(A=>C))), 'poi_000139_pm2.61d2', 0.11).
poi_theorem('pm2.61ii', ((n(A)=>(n(B)=>C))=>((A=>C)=>((B=>C)=>C))), 'poi_000140_pm2.61ii', 0.33).
poi_theorem('pm2.61nii', ((A=>(B=>C))=>((n(A)=>C)=>((n(B)=>C)=>C))), 'poi_000141_pm2.61nii', 0.44).
poi_theorem('pm2.61iii', ((n(A)=>(n(B)=>(n(C)=>D)))=>((A=>D)=>((B=>D)=>((C=>D)=>D)))), 'poi_000142_pm2.61iii', 1).
poi_theorem(ja, ((n(A)=>B)=>((C=>B)=>((A=>C)=>B))), poi_000143_ja, 0.33).
poi_theorem(jad, ((A=>(n(B)=>C))=>((A=>(D=>C))=>(A=>((B=>D)=>C)))), poi_000144_jad, 0.89).
poi_theorem('pm2.01', ((A=>n(A))=>n(A)), 'poi_000145_pm2.01', 0).
poi_theorem('pm2.01d', ((A=>(B=>n(B)))=>(A=>n(B))), 'poi_000146_pm2.01d', 0).
poi_theorem('pm2.6', ((n(A)=>B)=>((A=>B)=>B)), 'poi_000147_pm2.6', 0.11).
poi_theorem('pm2.61', ((A=>B)=>((n(A)=>B)=>B)), 'poi_000148_pm2.61', 0.11).
poi_theorem('pm2.65', ((A=>B)=>((A=>n(B))=>n(A))), 'poi_000149_pm2.65', 0.11).
poi_theorem('pm2.65d', ((A=>(B=>C))=>((A=>(B=>n(C)))=>(A=>n(B)))), 'poi_000150_pm2.65d', 0.33).
poi_theorem(mto, (n(A)=>((B=>A)=>n(B))), poi_000151_mto, 0.11).
poi_theorem(mtod, ((A=>n(B))=>((A=>(C=>B))=>(A=>n(C)))), poi_000152_mtod, 0.22).
poi_theorem(mtoi, (n(A)=>((B=>(C=>A))=>(B=>n(C)))), poi_000153_mtoi, 0.33).
poi_theorem(mt2, (A=>((B=>n(A))=>n(B))), poi_000154_mt2, 0).
poi_theorem(peirce, (((A=>_)=>A)=>A), poi_000155_peirce, 0).
poi_theorem(looinv, (((A=>B)=>B)=>((B=>A)=>A)), poi_000156_looinv, 0.11).
poi_theorem(bijust0, n(((A=>A)=>n((A=>A)))), poi_000157_bijust0, 0).
poi_theorem(bijust, n(((n(((A=>B)=>n((B=>A))))=>n(((A=>B)=>n((B=>A)))))=>n((n(((A=>B)=>n((B=>A))))=>n(((A=>B)=>n((B=>A)))))))), poi_000158_bijust, 0).
poi_theorem(impbi, ((A=>B)=>((B=>A)=>n(((A=>B)=>n((B=>A)))))), poi_000159_impbi, 0.22).
poi_theorem(impbidd, ((A=>(B=>(C=>D)))=>((A=>(B=>(D=>C)))=>(A=>(B=>n(((C=>D)=>n((D=>C)))))))), poi_000160_impbidd, 0.67).
poi_theorem(impbid21d, ((A=>(B=>C))=>((D=>(C=>B))=>(D=>(A=>n(((B=>C)=>n((C=>B)))))))), poi_000161_impbid21d, 0.33).
poi_theorem(impbid, ((A=>(B=>C))=>((A=>(C=>B))=>(A=>n(((B=>C)=>n((C=>B))))))), poi_000162_impbid, 0.44).
poi_theorem(biimp, (n(((A=>B)=>n((B=>A))))=>(A=>B)), poi_000163_biimp, 0).
poi_theorem(sylbi, (n(((A=>B)=>n((B=>A))))=>((B=>C)=>(A=>C))), poi_000164_sylbi, 0).
poi_theorem(sylib, ((A=>B)=>(n(((B=>C)=>n((C=>B))))=>(A=>C))), poi_000165_sylib, 0.11).
poi_theorem(sylbb, (n(((A=>B)=>n((B=>A))))=>(n(((B=>C)=>n((C=>B))))=>(A=>C))), poi_000166_sylbb, 0.11).
poi_theorem(biimpr, (n(((A=>B)=>n((B=>A))))=>(B=>A)), poi_000167_biimpr, 0).
poi_theorem(bicom1, (n(((A=>B)=>n((B=>A))))=>n(((B=>A)=>n((A=>B))))), poi_000168_bicom1, 0).
poi_theorem(bicom, n(((n(((A=>B)=>n((B=>A))))=>n(((B=>A)=>n((A=>B)))))=>n((n(((B=>A)=>n((A=>B))))=>n(((A=>B)=>n((B=>A)))))))), poi_000169_bicom, 0).
poi_theorem(bicomd, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((C=>B)=>n((B=>C)))))), poi_000170_bicomd, 0.22).
poi_theorem(impbid1, ((A=>(B=>C))=>((C=>B)=>(A=>n(((B=>C)=>n((C=>B))))))), poi_000171_impbid1, 0.33).
poi_theorem(impbid2, ((A=>B)=>((C=>(B=>A))=>(C=>n(((A=>B)=>n((B=>A))))))), poi_000172_impbid2, 0.22).
poi_theorem(impcon4bid, ((A=>(B=>C))=>((A=>(n(B)=>n(C)))=>(A=>n(((B=>C)=>n((C=>B))))))), poi_000173_impcon4bid, 0.89).
poi_theorem(biimpd, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>(B=>C))), poi_000174_biimpd, 0).
poi_theorem(mpbi, (A=>(n(((A=>B)=>n((B=>A))))=>B)), poi_000175_mpbi, 0).
poi_theorem(mpbir, (A=>(n(((B=>A)=>n((A=>B))))=>B)), poi_000176_mpbir, 0).
poi_theorem(mpbid, ((A=>B)=>((A=>n(((B=>C)=>n((C=>B)))))=>(A=>C))), poi_000177_mpbid, 0.22).
poi_theorem(mpbii, (A=>((B=>n(((A=>C)=>n((C=>A)))))=>(B=>C))), poi_000178_mpbii, 0.33).
poi_theorem(sylibr, ((A=>B)=>(n(((C=>B)=>n((B=>C))))=>(A=>C))), poi_000179_sylibr, 0.11).
poi_theorem(sylbir, (n(((A=>B)=>n((B=>A))))=>((A=>C)=>(B=>C))), poi_000180_sylbir, 0).
poi_theorem(sylbbr, (n(((A=>B)=>n((B=>A))))=>(n(((B=>C)=>n((C=>B))))=>(C=>A))), poi_000181_sylbbr, 0.11).
poi_theorem(sylbb1, (n(((A=>B)=>n((B=>A))))=>(n(((A=>C)=>n((C=>A))))=>(B=>C))), poi_000182_sylbb1, 0.11).
poi_theorem(sylbb2, (n(((A=>B)=>n((B=>A))))=>(n(((C=>B)=>n((B=>C))))=>(A=>C))), poi_000183_sylbb2, 0.11).
poi_theorem(sylibd, ((A=>(B=>C))=>((A=>n(((C=>D)=>n((D=>C)))))=>(A=>(B=>D)))), poi_000184_sylibd, 0.67).
poi_theorem(sylbid, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>(C=>D))=>(A=>(B=>D)))), poi_000185_sylbid, 0.67).
poi_theorem(mpbidi, ((A=>(B=>C))=>((B=>n(((C=>D)=>n((D=>C)))))=>(A=>(B=>D)))), poi_000186_mpbidi, 0.67).
poi_theorem(biimtrid, (n(((A=>B)=>n((B=>A))))=>((C=>(B=>D))=>(C=>(A=>D)))), poi_000187_biimtrid, 0.33).
poi_theorem(biimtrrid, (n(((A=>B)=>n((B=>A))))=>((C=>(A=>D))=>(C=>(B=>D)))), poi_000188_biimtrrid, 0.33).
poi_theorem(imbitrid, ((A=>B)=>((C=>n(((B=>D)=>n((D=>B)))))=>(C=>(A=>D)))), poi_000189_imbitrid, 0.33).
poi_theorem(syl5ibcom, ((A=>B)=>((C=>n(((B=>D)=>n((D=>B)))))=>(A=>(C=>D)))), poi_000190_syl5ibcom, 0.78).
poi_theorem(imbitrrid, ((A=>B)=>((C=>n(((D=>B)=>n((B=>D)))))=>(C=>(A=>D)))), poi_000191_imbitrrid, 0.33).
poi_theorem(syl5ibrcom, ((A=>B)=>((C=>n(((D=>B)=>n((B=>D)))))=>(A=>(C=>D)))), poi_000192_syl5ibrcom, 0.67).
poi_theorem(biimprd, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>(C=>B))), poi_000193_biimprd, 0).
poi_theorem(biimpcd, ((A=>n(((B=>C)=>n((C=>B)))))=>(B=>(A=>C))), poi_000194_biimpcd, 0.11).
poi_theorem(biimprcd, ((A=>n(((B=>C)=>n((C=>B)))))=>(C=>(A=>B))), poi_000195_biimprcd, 0).
poi_theorem(imbitrdi, ((A=>(B=>C))=>(n(((C=>D)=>n((D=>C))))=>(A=>(B=>D)))), poi_000196_imbitrdi, 0.33).
poi_theorem(imbitrrdi, ((A=>(B=>C))=>(n(((D=>C)=>n((C=>D))))=>(A=>(B=>D)))), poi_000197_imbitrrdi, 0.33).
poi_theorem(biimtrdi, ((A=>n(((B=>C)=>n((C=>B)))))=>((C=>D)=>(A=>(B=>D)))), poi_000198_biimtrdi, 0.67).
poi_theorem(biimtrrdi, ((A=>n(((B=>C)=>n((C=>B)))))=>((B=>D)=>(A=>(C=>D)))), poi_000199_biimtrrdi, 0.78).
poi_theorem(syl7bi, (n(((A=>B)=>n((B=>A))))=>((C=>(D=>(B=>E)))=>(C=>(D=>(A=>E))))), poi_000200_syl7bi, 0.33).
poi_theorem(syl8ib, ((A=>(B=>(C=>D)))=>(n(((D=>E)=>n((E=>D))))=>(A=>(B=>(C=>E))))), poi_000201_syl8ib, 0.33).
poi_theorem(mpbird, ((A=>B)=>((A=>n(((C=>B)=>n((B=>C)))))=>(A=>C))), poi_000202_mpbird, 0.22).
poi_theorem(mpbiri, (A=>((B=>n(((C=>A)=>n((A=>C)))))=>(B=>C))), poi_000203_mpbiri, 0.11).
poi_theorem(sylibrd, ((A=>(B=>C))=>((A=>n(((D=>C)=>n((C=>D)))))=>(A=>(B=>D)))), poi_000204_sylibrd, 0.67).
poi_theorem(sylbird, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>(B=>D))=>(A=>(C=>D)))), poi_000205_sylbird, 0.67).
poi_theorem(biidd, (_=>n(((A=>A)=>n((A=>A))))), poi_000206_biidd, 0).
poi_theorem('pm5.1im', (A=>(B=>n(((A=>B)=>n((B=>A)))))), 'poi_000207_pm5.1im', 0.22).
poi_theorem('2thd', ((A=>B)=>((A=>C)=>(A=>n(((B=>C)=>n((C=>B))))))), poi_000208_2thd, 0.33).
poi_theorem(monothetic, n((((A=>A)=>(B=>B))=>n(((B=>B)=>(A=>A))))), poi_000209_monothetic, 0).
poi_theorem(ibi, ((A=>n(((A=>B)=>n((B=>A)))))=>(A=>B)), poi_000210_ibi, 0).
poi_theorem(ibir, ((A=>n(((B=>A)=>n((A=>B)))))=>(A=>B)), poi_000211_ibir, 0).
poi_theorem(ibd, ((A=>(B=>n(((B=>C)=>n((C=>B))))))=>(A=>(B=>C))), poi_000212_ibd, 0).
poi_theorem('pm5.74', n((((A=>n(((B=>C)=>n((C=>B)))))=>n((((A=>B)=>(A=>C))=>n(((A=>C)=>(A=>B))))))=>n((n((((A=>B)=>(A=>C))=>n(((A=>C)=>(A=>B)))))=>(A=>n(((B=>C)=>n((C=>B))))))))), 'poi_000213_pm5.74', 1).
poi_theorem('pm5.74i', ((A=>n(((B=>C)=>n((C=>B)))))=>n((((A=>B)=>(A=>C))=>n(((A=>C)=>(A=>B)))))), 'poi_000214_pm5.74i', 0.89).
poi_theorem('pm5.74ri', (n((((A=>B)=>(A=>C))=>n(((A=>C)=>(A=>B)))))=>(A=>n(((B=>C)=>n((C=>B)))))), 'poi_000215_pm5.74ri', 1).
poi_theorem('pm5.74d', ((A=>(B=>n(((C=>D)=>n((D=>C))))))=>(A=>n((((B=>C)=>(B=>D))=>n(((B=>D)=>(B=>C))))))), 'poi_000216_pm5.74d', 1).
poi_theorem('pm5.74rd', ((A=>n((((B=>C)=>(B=>D))=>n(((B=>D)=>(B=>C))))))=>(A=>(B=>n(((C=>D)=>n((D=>C))))))), 'poi_000217_pm5.74rd', 1).
poi_theorem(bitri, (n(((A=>B)=>n((B=>A))))=>(n(((B=>C)=>n((C=>B))))=>n(((A=>C)=>n((C=>A)))))), poi_000218_bitri, 1).
poi_theorem(bitr2i, (n(((A=>B)=>n((B=>A))))=>(n(((B=>C)=>n((C=>B))))=>n(((C=>A)=>n((A=>C)))))), poi_000219_bitr2i, 1).
poi_theorem(bitr4i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>B)=>n((B=>C))))=>n(((A=>C)=>n((C=>A)))))), poi_000220_bitr4i, 1).
poi_theorem(bitrd, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((C=>D)=>n((D=>C)))))=>(A=>n(((B=>D)=>n((D=>B))))))), poi_000221_bitrd, 1).
poi_theorem(bitr2d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((C=>D)=>n((D=>C)))))=>(A=>n(((D=>B)=>n((B=>D))))))), poi_000222_bitr2d, 1).
poi_theorem(bitr3d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((B=>D)=>n((D=>B)))))=>(A=>n(((C=>D)=>n((D=>C))))))), poi_000223_bitr3d, 1).
poi_theorem(bitr4d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>C)=>n((C=>D)))))=>(A=>n(((B=>D)=>n((D=>B))))))), poi_000224_bitr4d, 1).
poi_theorem(bitrid, (n(((A=>B)=>n((B=>A))))=>((C=>n(((B=>D)=>n((D=>B)))))=>(C=>n(((A=>D)=>n((D=>A))))))), poi_000225_bitrid, 1).
poi_theorem(bitr2id, (n(((A=>B)=>n((B=>A))))=>((C=>n(((B=>D)=>n((D=>B)))))=>(C=>n(((D=>A)=>n((A=>D))))))), poi_000226_bitr2id, 1).
poi_theorem(bitr3id, (n(((A=>B)=>n((B=>A))))=>((C=>n(((A=>D)=>n((D=>A)))))=>(C=>n(((B=>D)=>n((D=>B))))))), poi_000227_bitr3id, 1).
poi_theorem(bitr3di, ((A=>n(((B=>C)=>n((C=>B)))))=>(n(((B=>D)=>n((D=>B))))=>(A=>n(((C=>D)=>n((D=>C))))))), poi_000228_bitr3di, 1).
poi_theorem(bitrdi, ((A=>n(((B=>C)=>n((C=>B)))))=>(n(((C=>D)=>n((D=>C))))=>(A=>n(((B=>D)=>n((D=>B))))))), poi_000229_bitrdi, 1).
poi_theorem(bitr2di, ((A=>n(((B=>C)=>n((C=>B)))))=>(n(((C=>D)=>n((D=>C))))=>(A=>n(((D=>B)=>n((B=>D))))))), poi_000230_bitr2di, 1).
poi_theorem(bitr4di, ((A=>n(((B=>C)=>n((C=>B)))))=>(n(((D=>C)=>n((C=>D))))=>(A=>n(((B=>D)=>n((D=>B))))))), poi_000231_bitr4di, 1).
poi_theorem(bitr4id, (n(((A=>B)=>n((B=>A))))=>((C=>n(((D=>B)=>n((B=>D)))))=>(C=>n(((A=>D)=>n((D=>A))))))), poi_000232_bitr4id, 1).
poi_theorem('3imtr3i', ((A=>B)=>(n(((A=>C)=>n((C=>A))))=>(n(((B=>D)=>n((D=>B))))=>(C=>D)))), poi_000233_3imtr3i, 0.78).
poi_theorem('3imtr4i', ((A=>B)=>(n(((C=>A)=>n((A=>C))))=>(n(((D=>B)=>n((B=>D))))=>(C=>D)))), poi_000234_3imtr4i, 0.78).
poi_theorem('3imtr3d', ((A=>(B=>C))=>((A=>n(((B=>D)=>n((D=>B)))))=>((A=>n(((C=>E)=>n((E=>C)))))=>(A=>(D=>E))))), poi_000235_3imtr3d, 1).
poi_theorem('3imtr4d', ((A=>(B=>C))=>((A=>n(((D=>B)=>n((B=>D)))))=>((A=>n(((E=>C)=>n((C=>E)))))=>(A=>(D=>E))))), poi_000236_3imtr4d, 1).
poi_theorem('3imtr3g', ((A=>(B=>C))=>(n(((B=>D)=>n((D=>B))))=>(n(((C=>E)=>n((E=>C))))=>(A=>(D=>E))))), poi_000237_3imtr3g, 1).
poi_theorem('3imtr4g', ((A=>(B=>C))=>(n(((D=>B)=>n((B=>D))))=>(n(((E=>C)=>n((C=>E))))=>(A=>(D=>E))))), poi_000238_3imtr4g, 1).
poi_theorem('3bitri', (n(((A=>B)=>n((B=>A))))=>(n(((B=>C)=>n((C=>B))))=>(n(((C=>D)=>n((D=>C))))=>n(((A=>D)=>n((D=>A))))))), poi_000239_3bitri, 1).
poi_theorem('3bitrri', (n(((A=>B)=>n((B=>A))))=>(n(((B=>C)=>n((C=>B))))=>(n(((C=>D)=>n((D=>C))))=>n(((D=>A)=>n((A=>D))))))), poi_000240_3bitrri, 1).
poi_theorem('3bitr2i', (n(((A=>B)=>n((B=>A))))=>(n(((C=>B)=>n((B=>C))))=>(n(((C=>D)=>n((D=>C))))=>n(((A=>D)=>n((D=>A))))))), poi_000241_3bitr2i, 1).
poi_theorem('3bitr2ri', (n(((A=>B)=>n((B=>A))))=>(n(((C=>B)=>n((B=>C))))=>(n(((C=>D)=>n((D=>C))))=>n(((D=>A)=>n((A=>D))))))), poi_000242_3bitr2ri, 1).
poi_theorem('3bitr3i', (n(((A=>B)=>n((B=>A))))=>(n(((A=>C)=>n((C=>A))))=>(n(((B=>D)=>n((D=>B))))=>n(((C=>D)=>n((D=>C))))))), poi_000243_3bitr3i, 1).
poi_theorem('3bitr3ri', (n(((A=>B)=>n((B=>A))))=>(n(((A=>C)=>n((C=>A))))=>(n(((B=>D)=>n((D=>B))))=>n(((D=>C)=>n((C=>D))))))), poi_000244_3bitr3ri, 1).
poi_theorem('3bitr4i', (n(((A=>B)=>n((B=>A))))=>(n(((C=>A)=>n((A=>C))))=>(n(((D=>B)=>n((B=>D))))=>n(((C=>D)=>n((D=>C))))))), poi_000245_3bitr4i, 1).
poi_theorem('3bitr4ri', (n(((A=>B)=>n((B=>A))))=>(n(((C=>A)=>n((A=>C))))=>(n(((D=>B)=>n((B=>D))))=>n(((D=>C)=>n((C=>D))))))), poi_000246_3bitr4ri, 1).
poi_theorem('3bitrd', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((C=>D)=>n((D=>C)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((B=>E)=>n((E=>B)))))))), poi_000247_3bitrd, 1).
poi_theorem('3bitrrd', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((C=>D)=>n((D=>C)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((E=>B)=>n((B=>E)))))))), poi_000248_3bitrrd, 1).
poi_theorem('3bitr2d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>C)=>n((C=>D)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((B=>E)=>n((E=>B)))))))), poi_000249_3bitr2d, 1).
poi_theorem('3bitr2rd', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>C)=>n((C=>D)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((E=>B)=>n((B=>E)))))))), poi_000250_3bitr2rd, 1).
poi_theorem('3bitr3d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((B=>D)=>n((D=>B)))))=>((A=>n(((C=>E)=>n((E=>C)))))=>(A=>n(((D=>E)=>n((E=>D)))))))), poi_000251_3bitr3d, 1).
poi_theorem('3bitr3rd', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((B=>D)=>n((D=>B)))))=>((A=>n(((C=>E)=>n((E=>C)))))=>(A=>n(((E=>D)=>n((D=>E)))))))), poi_000252_3bitr3rd, 1).
poi_theorem('3bitr4d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>B)=>n((B=>D)))))=>((A=>n(((E=>C)=>n((C=>E)))))=>(A=>n(((D=>E)=>n((E=>D)))))))), poi_000253_3bitr4d, 1).
poi_theorem('3bitr4rd', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>B)=>n((B=>D)))))=>((A=>n(((E=>C)=>n((C=>E)))))=>(A=>n(((E=>D)=>n((D=>E)))))))), poi_000254_3bitr4rd, 1).
poi_theorem('3bitr3g', ((A=>n(((B=>C)=>n((C=>B)))))=>(n(((B=>D)=>n((D=>B))))=>(n(((C=>E)=>n((E=>C))))=>(A=>n(((D=>E)=>n((E=>D)))))))), poi_000255_3bitr3g, 1).
poi_theorem('3bitr4g', ((A=>n(((B=>C)=>n((C=>B)))))=>(n(((D=>B)=>n((B=>D))))=>(n(((E=>C)=>n((C=>E))))=>(A=>n(((D=>E)=>n((E=>D)))))))), poi_000256_3bitr4g, 1).
poi_theorem(notnotb, n(((A=>n(n(A)))=>n((n(n(A))=>A)))), poi_000257_notnotb, 0).
poi_theorem(con34b, n((((A=>B)=>(n(B)=>n(A)))=>n(((n(B)=>n(A))=>(A=>B))))), poi_000258_con34b, 0).
poi_theorem(con4bid, ((A=>n(((n(B)=>n(C))=>n((n(C)=>n(B))))))=>(A=>n(((B=>C)=>n((C=>B)))))), poi_000259_con4bid, 0.44).
poi_theorem(notbid, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n(B)=>n(C))=>n((n(C)=>n(B))))))), poi_000260_notbid, 0.44).
poi_theorem(notbi, n(((n(((A=>B)=>n((B=>A))))=>n(((n(A)=>n(B))=>n((n(B)=>n(A))))))=>n((n(((n(A)=>n(B))=>n((n(B)=>n(A)))))=>n(((A=>B)=>n((B=>A)))))))), poi_000261_notbi, 0.67).
poi_theorem(notbii, (n(((A=>B)=>n((B=>A))))=>n(((n(A)=>n(B))=>n((n(B)=>n(A)))))), poi_000262_notbii, 0.44).
poi_theorem(con4bii, (n(((n(A)=>n(B))=>n((n(B)=>n(A)))))=>n(((A=>B)=>n((B=>A))))), poi_000263_con4bii, 0.44).
poi_theorem(mtbi, (n(A)=>(n(((A=>B)=>n((B=>A))))=>n(B))), poi_000264_mtbi, 0.11).
poi_theorem(mtbir, (n(A)=>(n(((B=>A)=>n((A=>B))))=>n(B))), poi_000265_mtbir, 0.11).
poi_theorem(mtbid, ((A=>n(B))=>((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(C)))), poi_000266_mtbid, 0.67).
poi_theorem(mtbird, ((A=>n(B))=>((A=>n(((C=>B)=>n((B=>C)))))=>(A=>n(C)))), poi_000267_mtbird, 0.33).
poi_theorem(mtbii, (n(A)=>((B=>n(((A=>C)=>n((C=>A)))))=>(B=>n(C)))), poi_000268_mtbii, 0.33).
poi_theorem(mtbiri, (n(A)=>((B=>n(((C=>A)=>n((A=>C)))))=>(B=>n(C)))), poi_000269_mtbiri, 0.33).
poi_theorem(sylnib, ((A=>n(B))=>(n(((B=>C)=>n((C=>B))))=>(A=>n(C)))), poi_000270_sylnib, 0.11).
poi_theorem(sylnibr, ((A=>n(B))=>(n(((C=>B)=>n((B=>C))))=>(A=>n(C)))), poi_000271_sylnibr, 0.11).
poi_theorem(sylnbi, (n(((A=>B)=>n((B=>A))))=>((n(B)=>C)=>(n(A)=>C))), poi_000272_sylnbi, 0.11).
poi_theorem(sylnbir, (n(((A=>B)=>n((B=>A))))=>((n(A)=>C)=>(n(B)=>C))), poi_000273_sylnbir, 0.11).
poi_theorem(xchnxbi, (n(((n(A)=>B)=>n((B=>n(A)))))=>(n(((A=>C)=>n((C=>A))))=>n(((n(C)=>B)=>n((B=>n(C))))))), poi_000274_xchnxbi, 1).
poi_theorem(xchnxbir, (n(((n(A)=>B)=>n((B=>n(A)))))=>(n(((C=>A)=>n((A=>C))))=>n(((n(C)=>B)=>n((B=>n(C))))))), poi_000275_xchnxbir, 1).
poi_theorem(xchbinx, (n(((A=>n(B))=>n((n(B)=>A))))=>(n(((B=>C)=>n((C=>B))))=>n(((A=>n(C))=>n((n(C)=>A)))))), poi_000276_xchbinx, 1).
poi_theorem(xchbinxr, (n(((A=>n(B))=>n((n(B)=>A))))=>(n(((C=>B)=>n((B=>C))))=>n(((A=>n(C))=>n((n(C)=>A)))))), poi_000277_xchbinxr, 1).
poi_theorem(bibi2i, (n(((A=>B)=>n((B=>A))))=>n(((n(((C=>A)=>n((A=>C))))=>n(((C=>B)=>n((B=>C)))))=>n((n(((C=>B)=>n((B=>C))))=>n(((C=>A)=>n((A=>C))))))))), poi_000278_bibi2i, 1).
poi_theorem(bibi12i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n(((n(((A=>C)=>n((C=>A))))=>n(((B=>D)=>n((D=>B)))))=>n((n(((B=>D)=>n((D=>B))))=>n(((A=>C)=>n((C=>A)))))))))), poi_000279_bibi12i, 1).
poi_theorem(imbi2d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n((((D=>B)=>(D=>C))=>n(((D=>C)=>(D=>B))))))), poi_000280_imbi2d, 0.56).
poi_theorem(imbi1d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n((((B=>D)=>(C=>D))=>n(((C=>D)=>(B=>D))))))), poi_000281_imbi1d, 0.78).
poi_theorem(bibi2d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n(((D=>B)=>n((B=>D))))=>n(((D=>C)=>n((C=>D)))))=>n((n(((D=>C)=>n((C=>D))))=>n(((D=>B)=>n((B=>D)))))))))), poi_000282_bibi2d, 1).
poi_theorem(bibi1d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n(((B=>D)=>n((D=>B))))=>n(((C=>D)=>n((D=>C)))))=>n((n(((C=>D)=>n((D=>C))))=>n(((B=>D)=>n((D=>B)))))))))), poi_000283_bibi1d, 1).
poi_theorem(imbi12d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n((((B=>D)=>(C=>E))=>n(((C=>E)=>(B=>D)))))))), poi_000284_imbi12d, 1).
poi_theorem(bibi12d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n(((B=>D)=>n((D=>B))))=>n(((C=>E)=>n((E=>C)))))=>n((n(((C=>E)=>n((E=>C))))=>n(((B=>D)=>n((D=>B))))))))))), poi_000285_bibi12d, 1).
poi_theorem(imbi12, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n((((A=>C)=>(B=>D))=>n(((B=>D)=>(A=>C))))))), poi_000286_imbi12, 1).
poi_theorem(imbi1, (n(((A=>B)=>n((B=>A))))=>n((((A=>C)=>(B=>C))=>n(((B=>C)=>(A=>C)))))), poi_000287_imbi1, 0.78).
poi_theorem(imbi2, (n(((A=>B)=>n((B=>A))))=>n((((C=>A)=>(C=>B))=>n(((C=>B)=>(C=>A)))))), poi_000288_imbi2, 0.67).
poi_theorem(bibi1, (n(((A=>B)=>n((B=>A))))=>n(((n(((A=>C)=>n((C=>A))))=>n(((B=>C)=>n((C=>B)))))=>n((n(((B=>C)=>n((C=>B))))=>n(((A=>C)=>n((C=>A))))))))), poi_000289_bibi1, 1).
poi_theorem(bitr3, (n(((A=>B)=>n((B=>A))))=>(n(((A=>C)=>n((C=>A))))=>n(((B=>C)=>n((C=>B)))))), poi_000290_bitr3, 1).
poi_theorem(con2bi, n(((n(((A=>n(B))=>n((n(B)=>A))))=>n(((B=>n(A))=>n((n(A)=>B)))))=>n((n(((B=>n(A))=>n((n(A)=>B))))=>n(((A=>n(B))=>n((n(B)=>A)))))))), poi_000291_con2bi, 0.22).
poi_theorem(con2bid, ((A=>n(((B=>n(C))=>n((n(C)=>B)))))=>(A=>n(((C=>n(B))=>n((n(B)=>C)))))), poi_000292_con2bid, 0.33).
poi_theorem(con1bid, ((A=>n(((n(B)=>C)=>n((C=>n(B))))))=>(A=>n(((n(C)=>B)=>n((B=>n(C))))))), poi_000293_con1bid, 0.33).
poi_theorem(con1bii, (n(((n(A)=>B)=>n((B=>n(A)))))=>n(((n(B)=>A)=>n((A=>n(B)))))), poi_000294_con1bii, 0.33).
poi_theorem(con2bii, (n(((A=>n(B))=>n((n(B)=>A))))=>n(((B=>n(A))=>n((n(A)=>B))))), poi_000295_con2bii, 0.33).
poi_theorem(con1b, n((((n(A)=>B)=>(n(B)=>A))=>n(((n(B)=>A)=>(n(A)=>B))))), poi_000296_con1b, 0).
poi_theorem(con2b, n((((A=>n(B))=>(B=>n(A)))=>n(((B=>n(A))=>(A=>n(B)))))), poi_000297_con2b, 0).
poi_theorem(biimt, (A=>n(((B=>(A=>B))=>n(((A=>B)=>B))))), poi_000298_biimt, 0).
poi_theorem('pm5.5', (A=>n((((A=>B)=>B)=>n((B=>(A=>B)))))), 'poi_000299_pm5.5', 0).
poi_theorem(mt2bi, (A=>n(((n(B)=>(B=>n(A)))=>n(((B=>n(A))=>n(B)))))), poi_000300_mt2bi, 0).
poi_theorem(mtt, (n(A)=>n(((n(B)=>(B=>A))=>n(((B=>A)=>n(B)))))), poi_000301_mtt, 0.11).
poi_theorem(imnot, (n(A)=>n((((B=>A)=>n(B))=>n((n(B)=>(B=>A)))))), poi_000302_imnot, 0.11).
poi_theorem('pm5.501', (A=>n(((B=>n(((A=>B)=>n((B=>A)))))=>n((n(((A=>B)=>n((B=>A))))=>B))))), 'poi_000303_pm5.501', 0.44).
poi_theorem(ibib, n((((A=>B)=>(A=>n(((A=>B)=>n((B=>A))))))=>n(((A=>n(((A=>B)=>n((B=>A)))))=>(A=>B))))), poi_000304_ibib, 0).
poi_theorem(ibibr, n((((A=>B)=>(A=>n(((B=>A)=>n((A=>B))))))=>n(((A=>n(((B=>A)=>n((A=>B)))))=>(A=>B))))), poi_000305_ibibr, 0).
poi_theorem(tbt, (A=>n(((B=>n(((B=>A)=>n((A=>B)))))=>n((n(((B=>A)=>n((A=>B))))=>B))))), poi_000306_tbt, 0.67).
poi_theorem(nbn2, (n(A)=>n(((n(B)=>n(((A=>B)=>n((B=>A)))))=>n((n(((A=>B)=>n((B=>A))))=>n(B)))))), poi_000307_nbn2, 0.44).
poi_theorem(bibif, (n(A)=>n(((n(((B=>A)=>n((A=>B))))=>n(B))=>n((n(B)=>n(((B=>A)=>n((A=>B))))))))), poi_000308_bibif, 0.44).
poi_theorem(nbn, (n(A)=>n(((n(B)=>n(((B=>A)=>n((A=>B)))))=>n((n(((B=>A)=>n((A=>B))))=>n(B)))))), poi_000309_nbn, 0.33).
poi_theorem(nbn3, (A=>n(((n(B)=>n(((B=>n(A))=>n((n(A)=>B)))))=>n((n(((B=>n(A))=>n((n(A)=>B))))=>n(B)))))), poi_000310_nbn3, 0.44).
poi_theorem('pm5.21im', (n(A)=>(n(B)=>n(((A=>B)=>n((B=>A)))))), 'poi_000311_pm5.21im', 0.22).
poi_theorem('2falsed', ((A=>n(B))=>((A=>n(C))=>(A=>n(((B=>C)=>n((C=>B))))))), poi_000312_2falsed, 0.44).
poi_theorem('pm5.21ni', ((A=>B)=>((C=>B)=>(n(B)=>n(((A=>C)=>n((C=>A))))))), 'poi_000313_pm5.21ni', 0.78).
poi_theorem('pm5.21nii', ((A=>B)=>((C=>B)=>((B=>n(((A=>C)=>n((C=>A)))))=>n(((A=>C)=>n((C=>A))))))), 'poi_000314_pm5.21nii', 0.78).
poi_theorem('pm5.21ndd', ((A=>(B=>C))=>((A=>(D=>C))=>((A=>(C=>n(((B=>D)=>n((D=>B))))))=>(A=>n(((B=>D)=>n((D=>B)))))))), 'poi_000315_pm5.21ndd', 1).
poi_theorem(bija, ((A=>(B=>C))=>((n(A)=>(n(B)=>C))=>(n(((A=>B)=>n((B=>A))))=>C))), poi_000316_bija, 1).
poi_theorem('pm5.18', n(((n(((A=>B)=>n((B=>A))))=>n(n(((A=>n(B))=>n((n(B)=>A))))))=>n((n(n(((A=>n(B))=>n((n(B)=>A)))))=>n(((A=>B)=>n((B=>A)))))))), 'poi_000317_pm5.18', 0.78).
poi_theorem(xor3, n(((n(n(((A=>B)=>n((B=>A)))))=>n(((A=>n(B))=>n((n(B)=>A)))))=>n((n(((A=>n(B))=>n((n(B)=>A))))=>n(n(((A=>B)=>n((B=>A))))))))), poi_000318_xor3, 0.78).
poi_theorem(nbbn, n(((n(((n(A)=>B)=>n((B=>n(A)))))=>n(n(((A=>B)=>n((B=>A))))))=>n((n(n(((A=>B)=>n((B=>A)))))=>n(((n(A)=>B)=>n((B=>n(A))))))))), poi_000319_nbbn, 0.78).
poi_theorem(biass, n(((n(((n(((A=>B)=>n((B=>A))))=>C)=>n((C=>n(((A=>B)=>n((B=>A))))))))=>n(((A=>n(((B=>C)=>n((C=>B)))))=>n((n(((B=>C)=>n((C=>B))))=>A)))))=>n((n(((A=>n(((B=>C)=>n((C=>B)))))=>n((n(((B=>C)=>n((C=>B))))=>A))))=>n(((n(((A=>B)=>n((B=>A))))=>C)=>n((C=>n(((A=>B)=>n((B=>A)))))))))))), poi_000320_biass, 1).
poi_theorem(biluk, n(((n(((A=>B)=>n((B=>A))))=>n(((n(((C=>B)=>n((B=>C))))=>n(((A=>C)=>n((C=>A)))))=>n((n(((A=>C)=>n((C=>A))))=>n(((C=>B)=>n((B=>C)))))))))=>n((n(((n(((C=>B)=>n((B=>C))))=>n(((A=>C)=>n((C=>A)))))=>n((n(((A=>C)=>n((C=>A))))=>n(((C=>B)=>n((B=>C))))))))=>n(((A=>B)=>n((B=>A)))))))), poi_000321_biluk, 1).
poi_theorem('pm5.19', n(n(((A=>n(A))=>n((n(A)=>A))))), 'poi_000322_pm5.19', 0).
poi_theorem('bi2.04', n((((A=>(B=>C))=>(B=>(A=>C)))=>n(((B=>(A=>C))=>(A=>(B=>C)))))), 'poi_000323_bi2.04', 0).
poi_theorem('pm5.4', n((((A=>(A=>B))=>(A=>B))=>n(((A=>B)=>(A=>(A=>B)))))), 'poi_000324_pm5.4', 0).
poi_theorem(imdi, n((((A=>(B=>C))=>((A=>B)=>(A=>C)))=>n((((A=>B)=>(A=>C))=>(A=>(B=>C)))))), poi_000325_imdi, 0).
poi_theorem('pm5.41', n(((((A=>B)=>(A=>C))=>(A=>(B=>C)))=>n(((A=>(B=>C))=>((A=>B)=>(A=>C)))))), 'poi_000326_pm5.41', 0).
poi_theorem(imbibi, (n((((A=>B)=>C)=>n((C=>(A=>B)))))=>(A=>n(((B=>C)=>n((C=>B)))))), poi_000327_imbibi, 0.89).
poi_theorem('pm4.8', n((((A=>n(A))=>n(A))=>n((n(A)=>(A=>n(A)))))), 'poi_000328_pm4.8', 0).
poi_theorem('pm4.81', n((((n(A)=>A)=>A)=>n((A=>(n(A)=>A))))), 'poi_000329_pm4.81', 0).
poi_theorem(imim21b, ((A=>B)=>n(((((B=>C)=>(A=>D))=>(A=>(C=>D)))=>n(((A=>(C=>D))=>((B=>C)=>(A=>D))))))), poi_000330_imim21b, 0.44).
poi_theorem('pm4.63', n(((n((A=>n(B)))=>n((A=>n(B))))=>n((n((A=>n(B)))=>n((A=>n(B))))))), 'poi_000331_pm4.63', 0).
poi_theorem('pm4.67', n(((n((n(A)=>n(B)))=>n((n(A)=>n(B))))=>n((n((n(A)=>n(B)))=>n((n(A)=>n(B))))))), 'poi_000332_pm4.67', 0).
poi_theorem(imnan, n((((A=>n(B))=>n(n((A=>n(B)))))=>n((n(n((A=>n(B))))=>(A=>n(B)))))), poi_000333_imnan, 0).
poi_theorem(imnani, (n(n((A=>n(B))))=>(A=>n(B))), poi_000334_imnani, 0).
poi_theorem(iman, n((((A=>B)=>n(n((A=>n(n(B))))))=>n((n(n((A=>n(n(B)))))=>(A=>B))))), poi_000335_iman, 0).
poi_theorem('pm3.24', n(n((A=>n(n(A))))), 'poi_000336_pm3.24', 0).
poi_theorem(annim, n(((n((A=>n(n(B))))=>n((A=>B)))=>n((n((A=>B))=>n((A=>n(n(B)))))))), poi_000337_annim, 0).
poi_theorem('pm4.61', n(((n((A=>B))=>n((A=>n(n(B)))))=>n((n((A=>n(n(B))))=>n((A=>B)))))), 'poi_000338_pm4.61', 0).
poi_theorem('pm4.65', n(((n((n(A)=>B))=>n((n(A)=>n(n(B)))))=>n((n((n(A)=>n(n(B))))=>n((n(A)=>B)))))), 'poi_000339_pm4.65', 0).
poi_theorem(impcom, ((A=>(B=>C))=>(n((B=>n(A)))=>C)), poi_000340_impcom, 0).
poi_theorem(con3dimp, ((A=>(B=>C))=>(n((A=>n(n(C))))=>n(B))), poi_000341_con3dimp, 0.11).
poi_theorem(mpnanrd, ((A=>B)=>((A=>n(n((B=>n(C)))))=>(A=>n(C)))), poi_000342_mpnanrd, 0.22).
poi_theorem(impd, ((A=>(B=>(C=>D)))=>(A=>(n((B=>n(C)))=>D))), poi_000343_impd, 0.11).
poi_theorem(impcomd, ((A=>(B=>(C=>D)))=>(A=>(n((C=>n(B)))=>D))), poi_000344_impcomd, 0.11).
poi_theorem(expcom, ((n((A=>n(B)))=>C)=>(B=>(A=>C))), poi_000345_expcom, 0.11).
poi_theorem(expdcom, ((A=>(n((B=>n(C)))=>D))=>(B=>(C=>(A=>D)))), poi_000346_expdcom, 0.67).
poi_theorem(expd, ((A=>(n((B=>n(C)))=>D))=>(A=>(B=>(C=>D)))), poi_000347_expd, 0.11).
poi_theorem(expcomd, ((A=>(n((B=>n(C)))=>D))=>(A=>(C=>(B=>D)))), poi_000348_expcomd, 0.33).
poi_theorem(imp31, ((A=>(B=>(C=>D)))=>(n((n((A=>n(B)))=>n(C)))=>D)), poi_000349_imp31, 0.44).
poi_theorem(imp32, ((A=>(B=>(C=>D)))=>(n((A=>n(n((B=>n(C))))))=>D)), poi_000350_imp32, 0.67).
poi_theorem(exp31, ((n((n((A=>n(B)))=>n(C)))=>D)=>(A=>(B=>(C=>D)))), poi_000351_exp31, 0.11).
poi_theorem(exp32, ((n((A=>n(n((B=>n(C))))))=>D)=>(A=>(B=>(C=>D)))), poi_000352_exp32, 0.11).
poi_theorem(imp4b, ((A=>(B=>(C=>(D=>E))))=>(n((A=>n(B)))=>(n((C=>n(D)))=>E))), poi_000353_imp4b, 0.78).
poi_theorem(imp4a, ((A=>(B=>(C=>(D=>E))))=>(A=>(B=>(n((C=>n(D)))=>E)))), poi_000354_imp4a, 0.33).
poi_theorem(imp4c, ((A=>(B=>(C=>(D=>E))))=>(A=>(n((n((B=>n(C)))=>n(D)))=>E))), poi_000355_imp4c, 0.67).
poi_theorem(imp4d, ((A=>(B=>(C=>(D=>E))))=>(A=>(n((B=>n(n((C=>n(D))))))=>E))), poi_000356_imp4d, 0.78).
poi_theorem(imp41, ((A=>(B=>(C=>(D=>E))))=>(n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)), poi_000357_imp41, 1).
poi_theorem(imp42, ((A=>(B=>(C=>(D=>E))))=>(n((n((A=>n(n((B=>n(C))))))=>n(D)))=>E)), poi_000358_imp42, 1).
poi_theorem(imp43, ((A=>(B=>(C=>(D=>E))))=>(n((n((A=>n(B)))=>n(n((C=>n(D))))))=>E)), poi_000359_imp43, 0.78).
poi_theorem(imp44, ((A=>(B=>(C=>(D=>E))))=>(n((A=>n(n((n((B=>n(C)))=>n(D))))))=>E)), poi_000360_imp44, 1).
poi_theorem(imp45, ((A=>(B=>(C=>(D=>E))))=>(n((A=>n(n((B=>n(n((C=>n(D)))))))))=>E)), poi_000361_imp45, 0.78).
poi_theorem(exp4b, ((n((A=>n(B)))=>(n((C=>n(D)))=>E))=>(A=>(B=>(C=>(D=>E))))), poi_000362_exp4b, 1).
poi_theorem(exp4a, ((A=>(B=>(n((C=>n(D)))=>E)))=>(A=>(B=>(C=>(D=>E))))), poi_000363_exp4a, 0.33).
poi_theorem(exp4c, ((A=>(n((n((B=>n(C)))=>n(D)))=>E))=>(A=>(B=>(C=>(D=>E))))), poi_000364_exp4c, 0.89).
poi_theorem(exp4d, ((A=>(n((B=>n(n((C=>n(D))))))=>E))=>(A=>(B=>(C=>(D=>E))))), poi_000365_exp4d, 0.89).
poi_theorem(exp41, ((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)=>(A=>(B=>(C=>(D=>E))))), poi_000366_exp41, 1).
poi_theorem(exp42, ((n((n((A=>n(n((B=>n(C))))))=>n(D)))=>E)=>(A=>(B=>(C=>(D=>E))))), poi_000367_exp42, 1).
poi_theorem(exp43, ((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>E)=>(A=>(B=>(C=>(D=>E))))), poi_000368_exp43, 1).
poi_theorem(exp44, ((n((A=>n(n((n((B=>n(C)))=>n(D))))))=>E)=>(A=>(B=>(C=>(D=>E))))), poi_000369_exp44, 1).
poi_theorem(exp45, ((n((A=>n(n((B=>n(n((C=>n(D)))))))))=>E)=>(A=>(B=>(C=>(D=>E))))), poi_000370_exp45, 0.89).
poi_theorem(imp5d, ((A=>(B=>(C=>(D=>(E=>F)))))=>(n((n((A=>n(B)))=>n(C)))=>(n((D=>n(E)))=>F))), poi_000371_imp5d, 1).
poi_theorem(imp5a, ((A=>(B=>(C=>(D=>(E=>F)))))=>(A=>(B=>(C=>(n((D=>n(E)))=>F))))), poi_000372_imp5a, 0.33).
poi_theorem(imp5g, ((A=>(B=>(C=>(D=>(E=>F)))))=>(n((A=>n(B)))=>(n((n((C=>n(D)))=>n(E)))=>F))), poi_000373_imp5g, 1).
poi_theorem(imp55, ((A=>(B=>(C=>(D=>(E=>F)))))=>(n((n((A=>n(n((B=>n(n((C=>n(D)))))))))=>n(E)))=>F)), poi_000374_imp55, 1).
poi_theorem(imp511, ((A=>(B=>(C=>(D=>(E=>F)))))=>(n((A=>n(n((n((B=>n(n((C=>n(D))))))=>n(E))))))=>F)), poi_000375_imp511, 1).
poi_theorem(exp5c, ((A=>(n((B=>n(C)))=>(n((D=>n(E)))=>F)))=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_000376_exp5c, 0.78).
poi_theorem(exp5j, ((A=>(n((n((n((B=>n(C)))=>n(D)))=>n(E)))=>F))=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_000377_exp5j, 1).
poi_theorem(exp5l, ((A=>(n((n((B=>n(C)))=>n(n((D=>n(E))))))=>F))=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_000378_exp5l, 1).
poi_theorem(exp53, ((n((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n(E)))=>F)=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_000379_exp53, 1).
poi_theorem(impexp, n((((n((A=>n(B)))=>C)=>(A=>(B=>C)))=>n(((A=>(B=>C))=>(n((A=>n(B)))=>C))))), poi_000380_impexp, 0.11).
poi_theorem(impancom, ((n((A=>n(B)))=>(C=>D))=>(n((A=>n(C)))=>(B=>D))), poi_000381_impancom, 0.78).
poi_theorem(expdimp, ((A=>(n((B=>n(C)))=>D))=>(n((A=>n(B)))=>(C=>D))), poi_000382_expdimp, 0.78).
poi_theorem(expimpd, ((n((A=>n(B)))=>(C=>D))=>(A=>(n((B=>n(C)))=>D))), poi_000383_expimpd, 0.78).
poi_theorem(impr, ((n((A=>n(B)))=>(C=>D))=>(n((A=>n(n((B=>n(C))))))=>D)), poi_000384_impr, 0.78).
poi_theorem(impl, ((A=>(n((B=>n(C)))=>D))=>(n((n((A=>n(B)))=>n(C)))=>D)), poi_000385_impl, 0.67).
poi_theorem(expr, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(B)))=>(C=>D))), poi_000386_expr, 0.33).
poi_theorem(expl, ((n((n((A=>n(B)))=>n(C)))=>D)=>(A=>(n((B=>n(C)))=>D))), poi_000387_expl, 0.33).
poi_theorem(ancoms, ((n((A=>n(B)))=>C)=>(n((B=>n(A)))=>C)), poi_000388_ancoms, 0).
poi_theorem('pm3.22', (n((A=>n(B)))=>n((B=>n(A)))), 'poi_000389_pm3.22', 0).
poi_theorem(ancom, n(((n((A=>n(B)))=>n((B=>n(A))))=>n((n((B=>n(A)))=>n((A=>n(B))))))), poi_000390_ancom, 0).
poi_theorem(ancomd, ((A=>n((B=>n(C))))=>(A=>n((C=>n(B))))), poi_000391_ancomd, 0).
poi_theorem(biancomi, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>n(((A=>n((C=>n(B))))=>n((n((C=>n(B)))=>A))))), poi_000392_biancomi, 0.67).
poi_theorem(biancomd, ((A=>n(((B=>n((C=>n(D))))=>n((n((C=>n(D)))=>B)))))=>(A=>n(((B=>n((D=>n(C))))=>n((n((D=>n(C)))=>B)))))), poi_000393_biancomd, 0.67).
poi_theorem(ancomst, n((((n((A=>n(B)))=>C)=>(n((B=>n(A)))=>C))=>n(((n((B=>n(A)))=>C)=>(n((A=>n(B)))=>C))))), poi_000394_ancomst, 0.22).
poi_theorem(ancomsd, ((A=>(n((B=>n(C)))=>D))=>(A=>(n((C=>n(B)))=>D))), poi_000395_ancomsd, 0.22).
poi_theorem(anasss, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((A=>n(n((B=>n(C))))))=>D)), poi_000396_anasss, 0.44).
poi_theorem(anassrs, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((n((A=>n(B)))=>n(C)))=>D)), poi_000397_anassrs, 0.44).
poi_theorem(anass, n(((n((n((A=>n(B)))=>n(C)))=>n((A=>n(n((B=>n(C)))))))=>n((n((A=>n(n((B=>n(C))))))=>n((n((A=>n(B)))=>n(C))))))), poi_000398_anass, 0.33).
poi_theorem('pm3.21', (A=>(B=>n((B=>n(A))))), 'poi_000399_pm3.21', 0).
poi_theorem('pm3.43i', ((A=>B)=>((A=>C)=>(A=>n((B=>n(C)))))), 'poi_000400_pm3.43i', 0.22).
poi_theorem('pm3.43', (n(((A=>B)=>n((A=>C))))=>(A=>n((B=>n(C))))), 'poi_000401_pm3.43', 0.33).
poi_theorem(biimpa, ((A=>n(((B=>C)=>n((C=>B)))))=>(n((A=>n(B)))=>C)), poi_000402_biimpa, 0.33).
poi_theorem(biimpar, ((A=>n(((B=>C)=>n((C=>B)))))=>(n((A=>n(C)))=>B)), poi_000403_biimpar, 0.33).
poi_theorem(biimpac, ((A=>n(((B=>C)=>n((C=>B)))))=>(n((B=>n(A)))=>C)), poi_000404_biimpac, 0.33).
poi_theorem(biimparc, ((A=>n(((B=>C)=>n((C=>B)))))=>(n((C=>n(A)))=>B)), poi_000405_biimparc, 0.33).
poi_theorem(simpl, (n((A=>n(_)))=>A), poi_000406_simpl, 0).
poi_theorem(intnan, (n(A)=>n(n((_=>n(A))))), poi_000407_intnan, 0).
poi_theorem(intnanr, (n(A)=>n(n((A=>n(_))))), poi_000408_intnanr, 0).
poi_theorem(intnand, ((A=>n(B))=>(A=>n(n((_=>n(B)))))), poi_000409_intnand, 0).
poi_theorem(intnanrd, ((A=>n(B))=>(A=>n(n((B=>n(_)))))), poi_000410_intnanrd, 0).
poi_theorem(adantld, ((A=>(B=>C))=>(A=>(n((_=>n(B)))=>C))), poi_000411_adantld, 0).
poi_theorem(adantrd, ((A=>(B=>C))=>(A=>(n((B=>n(_)))=>C))), poi_000412_adantrd, 0).
poi_theorem('pm3.41', ((A=>B)=>(n((A=>n(_)))=>B)), 'poi_000413_pm3.41', 0).
poi_theorem('pm3.42', ((A=>B)=>(n((_=>n(A)))=>B)), 'poi_000414_pm3.42', 0).
poi_theorem(simpld, ((A=>n((B=>n(_))))=>(A=>B)), poi_000415_simpld, 0).
poi_theorem(simprd, ((A=>n((_=>n(B))))=>(A=>B)), poi_000416_simprd, 0).
poi_theorem(simprbi, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(A=>C)), poi_000417_simprbi, 0).
poi_theorem(simplbi, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(A=>B)), poi_000418_simplbi, 0).
poi_theorem(simprbda, ((A=>n(((B=>n((C=>n(D))))=>n((n((C=>n(D)))=>B)))))=>(n((A=>n(B)))=>C)), poi_000419_simprbda, 0.33).
poi_theorem(simplbda, ((A=>n(((B=>n((C=>n(D))))=>n((n((C=>n(D)))=>B)))))=>(n((A=>n(B)))=>D)), poi_000420_simplbda, 0.33).
poi_theorem(simplbi2, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(B=>(C=>A))), poi_000421_simplbi2, 0.11).
poi_theorem(simplbi2comt, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(C=>(B=>A))), poi_000422_simplbi2comt, 0.22).
poi_theorem(simpl2im, ((A=>n((_=>n(B))))=>((B=>C)=>(A=>C))), poi_000423_simpl2im, 0).
poi_theorem(simplbiim, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>((C=>D)=>(A=>D))), poi_000424_simplbiim, 0.33).
poi_theorem(impel, ((A=>(B=>C))=>((D=>B)=>(n((A=>n(D)))=>C))), poi_000425_impel, 0.33).
poi_theorem(mpan9, ((A=>B)=>((C=>(B=>D))=>(n((A=>n(C)))=>D))), poi_000426_mpan9, 0.33).
poi_theorem(sylan9, ((A=>(B=>C))=>((D=>(C=>E))=>(n((A=>n(D)))=>(B=>E)))), poi_000427_sylan9, 0.78).
poi_theorem(sylan9r, ((A=>(B=>C))=>((D=>(C=>E))=>(n((D=>n(A)))=>(B=>E)))), poi_000428_sylan9r, 0.78).
poi_theorem(sylan9bb, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(((C=>E)=>n((E=>C)))))=>(n((A=>n(D)))=>n(((B=>E)=>n((E=>B))))))), poi_000429_sylan9bb, 1).
poi_theorem(sylan9bbr, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(((C=>E)=>n((E=>C)))))=>(n((D=>n(A)))=>n(((B=>E)=>n((E=>B))))))), poi_000430_sylan9bbr, 1).
poi_theorem(jcad, ((A=>(B=>C))=>((A=>(B=>D))=>(A=>(B=>n((C=>n(D))))))), poi_000431_jcad, 0.78).
poi_theorem(jca2, ((A=>(B=>C))=>((B=>D)=>(A=>(B=>n((C=>n(D))))))), poi_000432_jca2, 0.56).
poi_theorem(jca31, ((A=>B)=>((A=>C)=>((A=>D)=>(A=>n((n((B=>n(C)))=>n(D))))))), poi_000433_jca31, 1).
poi_theorem(jca32, ((A=>B)=>((A=>C)=>((A=>D)=>(A=>n((B=>n(n((C=>n(D)))))))))), poi_000434_jca32, 0.78).
poi_theorem(jcai, ((A=>B)=>((A=>(B=>C))=>(A=>n((B=>n(C)))))), poi_000435_jcai, 0.22).
poi_theorem(jcab, n((((A=>n((B=>n(C))))=>n(((A=>B)=>n((A=>C)))))=>n((n(((A=>B)=>n((A=>C))))=>(A=>n((B=>n(C)))))))), poi_000436_jcab, 0.33).
poi_theorem('pm4.76', n(((n(((A=>B)=>n((A=>C))))=>(A=>n((B=>n(C)))))=>n(((A=>n((B=>n(C))))=>n(((A=>B)=>n((A=>C)))))))), 'poi_000437_pm4.76', 0.33).
poi_theorem(jctil, ((A=>B)=>(C=>(A=>n((C=>n(B)))))), poi_000438_jctil, 0).
poi_theorem(jctir, ((A=>B)=>(C=>(A=>n((B=>n(C)))))), poi_000439_jctir, 0).
poi_theorem(jccir, ((A=>B)=>((B=>C)=>(A=>n((B=>n(C)))))), poi_000440_jccir, 0).
poi_theorem(jccil, ((A=>B)=>((B=>C)=>(A=>n((C=>n(B)))))), poi_000441_jccil, 0.11).
poi_theorem(jctild, ((A=>(B=>C))=>((A=>D)=>(A=>(B=>n((D=>n(C))))))), poi_000442_jctild, 0.56).
poi_theorem(jctird, ((A=>(B=>C))=>((A=>D)=>(A=>(B=>n((C=>n(D))))))), poi_000443_jctird, 0.56).
poi_theorem(iba, (A=>n(((B=>n((B=>n(A))))=>n((n((B=>n(A)))=>B))))), poi_000444_iba, 0.11).
poi_theorem(ibar, (A=>n(((B=>n((A=>n(B))))=>n((n((A=>n(B)))=>B))))), poi_000445_ibar, 0.11).
poi_theorem(biantrud, ((A=>B)=>(A=>n(((C=>n((C=>n(B))))=>n((n((C=>n(B)))=>C)))))), poi_000446_biantrud, 0.11).
poi_theorem(biantrurd, ((A=>B)=>(A=>n(((C=>n((B=>n(C))))=>n((n((B=>n(C)))=>C)))))), poi_000447_biantrurd, 0.11).
poi_theorem(bianfi, (n(A)=>n(((A=>n((B=>n(A))))=>n((n((B=>n(A)))=>A))))), poi_000448_bianfi, 0.11).
poi_theorem(bianfd, ((A=>n(B))=>(A=>n(((B=>n((B=>n(C))))=>n((n((B=>n(C)))=>B)))))), poi_000449_bianfd, 0.11).
poi_theorem(baib, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(B=>n(((A=>C)=>n((C=>A)))))), poi_000450_baib, 1).
poi_theorem(baibr, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(B=>n(((C=>A)=>n((A=>C)))))), poi_000451_baibr, 1).
poi_theorem(rbaibr, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(C=>n(((B=>A)=>n((A=>B)))))), poi_000452_rbaibr, 1).
poi_theorem(rbaib, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(C=>n(((A=>B)=>n((B=>A)))))), poi_000453_rbaib, 1).
poi_theorem(baibd, ((A=>n(((B=>n((C=>n(D))))=>n((n((C=>n(D)))=>B)))))=>(n((A=>n(C)))=>n(((B=>D)=>n((D=>B)))))), poi_000454_baibd, 1).
poi_theorem(rbaibd, ((A=>n(((B=>n((C=>n(D))))=>n((n((C=>n(D)))=>B)))))=>(n((A=>n(D)))=>n(((B=>C)=>n((C=>B)))))), poi_000455_rbaibd, 1).
poi_theorem(bianabs, ((A=>n(((B=>n((A=>n(C))))=>n((n((A=>n(C)))=>B)))))=>(A=>n(((B=>C)=>n((C=>B)))))), poi_000456_bianabs, 1).
poi_theorem('pm5.44', ((A=>B)=>n((((A=>C)=>(A=>n((B=>n(C)))))=>n(((A=>n((B=>n(C))))=>(A=>C)))))), 'poi_000457_pm5.44', 0.33).
poi_theorem('pm5.42', n((((A=>(B=>C))=>(A=>(B=>n((A=>n(C))))))=>n(((A=>(B=>n((A=>n(C)))))=>(A=>(B=>C)))))), 'poi_000458_pm5.42', 0.22).
poi_theorem(ancl, ((A=>B)=>(A=>n((A=>n(B))))), poi_000459_ancl, 0).
poi_theorem(anclb, n((((A=>B)=>(A=>n((A=>n(B)))))=>n(((A=>n((A=>n(B))))=>(A=>B))))), poi_000460_anclb, 0.22).
poi_theorem(ancr, ((A=>B)=>(A=>n((B=>n(A))))), poi_000461_ancr, 0).
poi_theorem(ancrb, n((((A=>B)=>(A=>n((B=>n(A)))))=>n(((A=>n((B=>n(A))))=>(A=>B))))), poi_000462_ancrb, 0).
poi_theorem(ancld, ((A=>(B=>C))=>(A=>(B=>n((B=>n(C)))))), poi_000463_ancld, 0).
poi_theorem(ancrd, ((A=>(B=>C))=>(A=>(B=>n((C=>n(B)))))), poi_000464_ancrd, 0).
poi_theorem(impac, ((A=>(B=>C))=>(n((A=>n(B)))=>n((C=>n(B))))), poi_000465_impac, 0.11).
poi_theorem(anc2l, ((A=>(B=>C))=>(A=>(B=>n((A=>n(C)))))), poi_000466_anc2l, 0).
poi_theorem(anc2r, ((A=>(B=>C))=>(A=>(B=>n((C=>n(A)))))), poi_000467_anc2r, 0).
poi_theorem('pm4.71', n((((A=>B)=>n(((A=>n((A=>n(B))))=>n((n((A=>n(B)))=>A)))))=>n((n(((A=>n((A=>n(B))))=>n((n((A=>n(B)))=>A))))=>(A=>B))))), 'poi_000468_pm4.71', 0.11).
poi_theorem('pm4.71r', n((((A=>B)=>n(((A=>n((B=>n(A))))=>n((n((B=>n(A)))=>A)))))=>n((n(((A=>n((B=>n(A))))=>n((n((B=>n(A)))=>A))))=>(A=>B))))), 'poi_000469_pm4.71r', 0.11).
poi_theorem('pm4.71i', ((A=>B)=>n(((A=>n((A=>n(B))))=>n((n((A=>n(B)))=>A))))), 'poi_000470_pm4.71i', 0.11).
poi_theorem('pm4.71ri', ((A=>B)=>n(((A=>n((B=>n(A))))=>n((n((B=>n(A)))=>A))))), 'poi_000471_pm4.71ri', 0.11).
poi_theorem('pm4.71d', ((A=>(B=>C))=>(A=>n(((B=>n((B=>n(C))))=>n((n((B=>n(C)))=>B)))))), 'poi_000472_pm4.71d', 0.11).
poi_theorem('pm4.71rd', ((A=>(B=>C))=>(A=>n(((B=>n((C=>n(B))))=>n((n((C=>n(B)))=>B)))))), 'poi_000473_pm4.71rd', 0.11).
poi_theorem('pm4.24', n(((A=>n((A=>n(A))))=>n((n((A=>n(A)))=>A)))), 'poi_000474_pm4.24', 0).
poi_theorem(anidm, n(((n((A=>n(A)))=>A)=>n((A=>n((A=>n(A))))))), poi_000475_anidm, 0).
poi_theorem(anidmdbi, n((((A=>n((B=>n(B))))=>(A=>B))=>n(((A=>B)=>(A=>n((B=>n(B)))))))), poi_000476_anidmdbi, 0).
poi_theorem(anidms, ((n((A=>n(A)))=>B)=>(A=>B)), poi_000477_anidms, 0).
poi_theorem(imdistan, n((((A=>(B=>C))=>(n((A=>n(B)))=>n((A=>n(C)))))=>n(((n((A=>n(B)))=>n((A=>n(C))))=>(A=>(B=>C)))))), poi_000478_imdistan, 0.33).
poi_theorem(imdistani, ((A=>(B=>C))=>(n((A=>n(B)))=>n((A=>n(C))))), poi_000479_imdistani, 0.44).
poi_theorem(imdistanri, ((A=>(B=>C))=>(n((B=>n(A)))=>n((C=>n(A))))), poi_000480_imdistanri, 0.33).
poi_theorem(imdistand, ((A=>(B=>(C=>D)))=>(A=>(n((B=>n(C)))=>n((B=>n(D)))))), poi_000481_imdistand, 0.78).
poi_theorem(imdistanda, ((n((A=>n(B)))=>(C=>D))=>(A=>(n((B=>n(C)))=>n((B=>n(D)))))), poi_000482_imdistanda, 0.78).
poi_theorem('pm5.3', n((((n((A=>n(B)))=>C)=>(n((A=>n(B)))=>n((A=>n(C)))))=>n(((n((A=>n(B)))=>n((A=>n(C))))=>(n((A=>n(B)))=>C))))), 'poi_000483_pm5.3', 0).
poi_theorem('pm5.32', n((((A=>n(((B=>C)=>n((C=>B)))))=>n(((n((A=>n(B)))=>n((A=>n(C))))=>n((n((A=>n(C)))=>n((A=>n(B))))))))=>n((n(((n((A=>n(B)))=>n((A=>n(C))))=>n((n((A=>n(C)))=>n((A=>n(B)))))))=>(A=>n(((B=>C)=>n((C=>B))))))))), 'poi_000484_pm5.32', 1).
poi_theorem('pm5.32i', ((A=>n(((B=>C)=>n((C=>B)))))=>n(((n((A=>n(B)))=>n((A=>n(C))))=>n((n((A=>n(C)))=>n((A=>n(B)))))))), 'poi_000485_pm5.32i', 1).
poi_theorem('pm5.32ri', ((A=>n(((B=>C)=>n((C=>B)))))=>n(((n((B=>n(A)))=>n((C=>n(A))))=>n((n((C=>n(A)))=>n((B=>n(A)))))))), 'poi_000486_pm5.32ri', 1).
poi_theorem('pm5.32d', ((A=>(B=>n(((C=>D)=>n((D=>C))))))=>(A=>n(((n((B=>n(C)))=>n((B=>n(D))))=>n((n((B=>n(D)))=>n((B=>n(C))))))))), 'poi_000487_pm5.32d', 1).
poi_theorem('pm5.32rd', ((A=>(B=>n(((C=>D)=>n((D=>C))))))=>(A=>n(((n((C=>n(B)))=>n((D=>n(B))))=>n((n((D=>n(B)))=>n((C=>n(B))))))))), 'poi_000488_pm5.32rd', 1).
poi_theorem('pm5.32da', ((n((A=>n(B)))=>n(((C=>D)=>n((D=>C)))))=>(A=>n(((n((B=>n(C)))=>n((B=>n(D))))=>n((n((B=>n(D)))=>n((B=>n(C))))))))), 'poi_000489_pm5.32da', 1).
poi_theorem(sylan, ((A=>B)=>((n((B=>n(C)))=>D)=>(n((A=>n(C)))=>D))), poi_000490_sylan, 0.11).
poi_theorem(sylanb, (n(((A=>B)=>n((B=>A))))=>((n((B=>n(C)))=>D)=>(n((A=>n(C)))=>D))), poi_000491_sylanb, 0.89).
poi_theorem(sylanbr, (n(((A=>B)=>n((B=>A))))=>((n((A=>n(C)))=>D)=>(n((B=>n(C)))=>D))), poi_000492_sylanbr, 1).
poi_theorem(sylanbrc, ((A=>B)=>((A=>C)=>(n(((D=>n((B=>n(C))))=>n((n((B=>n(C)))=>D))))=>(A=>D)))), poi_000493_sylanbrc, 1).
poi_theorem(syl2anc, ((A=>B)=>((A=>C)=>((n((B=>n(C)))=>D)=>(A=>D)))), poi_000494_syl2anc, 0.78).
poi_theorem(syl2anc2, ((A=>B)=>((B=>C)=>((n((B=>n(C)))=>D)=>(A=>D)))), poi_000495_syl2anc2, 0.78).
poi_theorem(sylancl, ((A=>B)=>(C=>((n((B=>n(C)))=>D)=>(A=>D)))), poi_000496_sylancl, 0.78).
poi_theorem(sylancr, (A=>((B=>C)=>((n((A=>n(C)))=>D)=>(B=>D)))), poi_000497_sylancr, 0.78).
poi_theorem(sylancom, ((n((A=>n(B)))=>C)=>((n((C=>n(B)))=>D)=>(n((A=>n(B)))=>D))), poi_000498_sylancom, 0.67).
poi_theorem(sylanblc, ((A=>B)=>(C=>(n(((n((B=>n(C)))=>D)=>n((D=>n((B=>n(C)))))))=>(A=>D)))), poi_000499_sylanblc, 1).
poi_theorem(sylanblrc, ((A=>B)=>(C=>(n(((D=>n((B=>n(C))))=>n((n((B=>n(C)))=>D))))=>(A=>D)))), poi_000500_sylanblrc, 1).
poi_theorem(syldan, ((n((A=>n(B)))=>C)=>((n((A=>n(C)))=>D)=>(n((A=>n(B)))=>D))), poi_000501_syldan, 0.78).
poi_theorem(sylbida, ((A=>n(((B=>C)=>n((C=>B)))))=>((n((A=>n(C)))=>D)=>(n((A=>n(B)))=>D))), poi_000502_sylbida, 1).
poi_theorem(sylan2, ((A=>B)=>((n((C=>n(B)))=>D)=>(n((C=>n(A)))=>D))), poi_000503_sylan2, 0.78).
poi_theorem(sylan2b, (n(((A=>B)=>n((B=>A))))=>((n((C=>n(B)))=>D)=>(n((C=>n(A)))=>D))), poi_000504_sylan2b, 1).
poi_theorem(sylan2br, (n(((A=>B)=>n((B=>A))))=>((n((C=>n(A)))=>D)=>(n((C=>n(B)))=>D))), poi_000505_sylan2br, 1).
poi_theorem(syl2an, ((A=>B)=>((C=>D)=>((n((B=>n(D)))=>E)=>(n((A=>n(C)))=>E)))), poi_000506_syl2an, 0.78).
poi_theorem(syl2anr, ((A=>B)=>((C=>D)=>((n((B=>n(D)))=>E)=>(n((C=>n(A)))=>E)))), poi_000507_syl2anr, 0.78).
poi_theorem(syl2anb, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>((n((B=>n(D)))=>E)=>(n((A=>n(C)))=>E)))), poi_000508_syl2anb, 1).
poi_theorem(syl2anbr, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>((n((A=>n(C)))=>E)=>(n((B=>n(D)))=>E)))), poi_000509_syl2anbr, 1).
poi_theorem(sylancb, (n(((A=>B)=>n((B=>A))))=>(n(((A=>C)=>n((C=>A))))=>((n((B=>n(C)))=>D)=>(A=>D)))), poi_000510_sylancb, 1).
poi_theorem(sylancbr, (n(((A=>B)=>n((B=>A))))=>(n(((C=>B)=>n((B=>C))))=>((n((A=>n(C)))=>D)=>(B=>D)))), poi_000511_sylancbr, 1).
poi_theorem(syldanl, ((n((A=>n(B)))=>C)=>((n((n((A=>n(C)))=>n(D)))=>E)=>(n((n((A=>n(B)))=>n(D)))=>E))), poi_000512_syldanl, 0.78).
poi_theorem(syland, ((A=>(B=>C))=>((A=>(n((C=>n(D)))=>E))=>(A=>(n((B=>n(D)))=>E)))), poi_000513_syland, 1).
poi_theorem(sylani, ((A=>B)=>((C=>(n((B=>n(D)))=>E))=>(C=>(n((A=>n(D)))=>E)))), poi_000514_sylani, 1).
poi_theorem(sylan2d, ((A=>(B=>C))=>((A=>(n((D=>n(C)))=>E))=>(A=>(n((D=>n(B)))=>E)))), poi_000515_sylan2d, 1).
poi_theorem(sylan2i, ((A=>B)=>((C=>(n((D=>n(B)))=>E))=>(C=>(n((D=>n(A)))=>E)))), poi_000516_sylan2i, 1).
poi_theorem(syl2ani, ((A=>B)=>((C=>D)=>((E=>(n((B=>n(D)))=>F))=>(E=>(n((A=>n(C)))=>F))))), poi_000517_syl2ani, 1).
poi_theorem(syl2and, ((A=>(B=>C))=>((A=>(D=>E))=>((A=>(n((C=>n(E)))=>F))=>(A=>(n((B=>n(D)))=>F))))), poi_000518_syl2and, 1).
poi_theorem(anim12d, ((A=>(B=>C))=>((A=>(D=>E))=>(A=>(n((B=>n(D)))=>n((C=>n(E))))))), poi_000519_anim12d, 1).
poi_theorem(anim12d1, ((A=>(B=>C))=>((D=>E)=>(A=>(n((B=>n(D)))=>n((C=>n(E))))))), poi_000520_anim12d1, 0.78).
poi_theorem(anim1d, ((A=>(B=>C))=>(A=>(n((B=>n(D)))=>n((C=>n(D)))))), poi_000521_anim1d, 0.33).
poi_theorem(anim2d, ((A=>(B=>C))=>(A=>(n((D=>n(B)))=>n((D=>n(C)))))), poi_000522_anim2d, 0.33).
poi_theorem(anim12i, ((A=>B)=>((C=>D)=>(n((A=>n(C)))=>n((B=>n(D)))))), poi_000523_anim12i, 0.11).
poi_theorem(anim12ci, ((A=>B)=>((C=>D)=>(n((A=>n(C)))=>n((D=>n(B)))))), poi_000524_anim12ci, 0.11).
poi_theorem(anim1ci, ((A=>B)=>(n((A=>n(C)))=>n((C=>n(B))))), poi_000525_anim1ci, 0.11).
poi_theorem(anim2i, ((A=>B)=>(n((C=>n(A)))=>n((C=>n(B))))), poi_000526_anim2i, 0.11).
poi_theorem(anim12ii, ((A=>(B=>C))=>((D=>(B=>E))=>(n((A=>n(D)))=>(B=>n((C=>n(E))))))), poi_000527_anim12ii, 1).
poi_theorem(anim12dan, ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>E)=>(n((A=>n(n((B=>n(D))))))=>n((C=>n(E)))))), poi_000528_anim12dan, 1).
poi_theorem(im2anan9, ((A=>(B=>C))=>((D=>(E=>F))=>(n((A=>n(D)))=>(n((B=>n(E)))=>n((C=>n(F))))))), poi_000529_im2anan9, 1).
poi_theorem(im2anan9r, ((A=>(B=>C))=>((D=>(E=>F))=>(n((D=>n(A)))=>(n((B=>n(E)))=>n((C=>n(F))))))), poi_000530_im2anan9r, 0.78).
poi_theorem('pm3.45', ((A=>B)=>(n((A=>n(C)))=>n((B=>n(C))))), 'poi_000531_pm3.45', 0.11).
poi_theorem(anbi2ci, (n(((A=>B)=>n((B=>A))))=>n(((n((A=>n(C)))=>n((C=>n(B))))=>n((n((C=>n(B)))=>n((A=>n(C)))))))), poi_000532_anbi2ci, 1).
poi_theorem(anbi1ci, (n(((A=>B)=>n((B=>A))))=>n(((n((C=>n(A)))=>n((B=>n(C))))=>n((n((B=>n(C)))=>n((C=>n(A)))))))), poi_000533_anbi1ci, 1).
poi_theorem(bianbi, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(n(((B=>D)=>n((D=>B))))=>n(((A=>n((D=>n(C))))=>n((n((D=>n(C)))=>A)))))), poi_000534_bianbi, 1).
poi_theorem(anbi12i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n(((n((A=>n(C)))=>n((B=>n(D))))=>n((n((B=>n(D)))=>n((A=>n(C))))))))), poi_000535_anbi12i, 1).
poi_theorem(anbi12ci, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n(((n((A=>n(C)))=>n((D=>n(B))))=>n((n((D=>n(B)))=>n((A=>n(C))))))))), poi_000536_anbi12ci, 1).
poi_theorem(anbi2d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n((D=>n(B)))=>n((D=>n(C))))=>n((n((D=>n(C)))=>n((D=>n(B))))))))), poi_000537_anbi2d, 1).
poi_theorem(anbi1d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n((B=>n(D)))=>n((C=>n(D))))=>n((n((C=>n(D)))=>n((B=>n(D))))))))), poi_000538_anbi1d, 1).
poi_theorem(anbi12d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n((B=>n(D)))=>n((C=>n(E))))=>n((n((C=>n(E)))=>n((B=>n(D)))))))))), poi_000539_anbi12d, 1).
poi_theorem(anbi1, (n(((A=>B)=>n((B=>A))))=>n(((n((A=>n(C)))=>n((B=>n(C))))=>n((n((B=>n(C)))=>n((A=>n(C)))))))), poi_000540_anbi1, 1).
poi_theorem(anbi2, (n(((A=>B)=>n((B=>A))))=>n(((n((C=>n(A)))=>n((C=>n(B))))=>n((n((C=>n(B)))=>n((C=>n(A)))))))), poi_000541_anbi2, 1).
poi_theorem(anbi1cd, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n((D=>n(B)))=>n((C=>n(D))))=>n((n((C=>n(D)))=>n((D=>n(B))))))))), poi_000542_anbi1cd, 1).
poi_theorem(an2anr, n(((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n((n((B=>n(A)))=>n(n((D=>n(C)))))))=>n((n((n((B=>n(A)))=>n(n((D=>n(C))))))=>n((n((A=>n(B)))=>n(n((C=>n(D)))))))))), poi_000543_an2anr, 0.89).
poi_theorem('pm4.38', (n((n(((A=>B)=>n((B=>A))))=>n(n(((C=>D)=>n((D=>C)))))))=>n(((n((A=>n(C)))=>n((B=>n(D))))=>n((n((B=>n(D)))=>n((A=>n(C)))))))), 'poi_000544_pm4.38', 1).
poi_theorem(bi2anan9, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(((E=>F)=>n((F=>E)))))=>(n((A=>n(D)))=>n(((n((B=>n(E)))=>n((C=>n(F))))=>n((n((C=>n(F)))=>n((B=>n(E)))))))))), poi_000545_bi2anan9, 1).
poi_theorem(bi2anan9r, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(((E=>F)=>n((F=>E)))))=>(n((D=>n(A)))=>n(((n((B=>n(E)))=>n((C=>n(F))))=>n((n((C=>n(F)))=>n((B=>n(E)))))))))), poi_000546_bi2anan9r, 1).
poi_theorem(bi2bian9, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(((E=>F)=>n((F=>E)))))=>(n((A=>n(D)))=>n(((n(((B=>E)=>n((E=>B))))=>n(((C=>F)=>n((F=>C)))))=>n((n(((C=>F)=>n((F=>C))))=>n(((B=>E)=>n((E=>B))))))))))), poi_000547_bi2bian9, 1).
poi_theorem(anbiim, ((A=>(B=>C))=>((D=>(C=>B))=>(n((A=>n(D)))=>n(((B=>C)=>n((C=>B))))))), poi_000548_anbiim, 0.89).
poi_theorem(bianass, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>n(((n((D=>n(A)))=>n((n((D=>n(B)))=>n(C))))=>n((n((n((D=>n(B)))=>n(C)))=>n((D=>n(A)))))))), poi_000549_bianass, 1).
poi_theorem(bianassc, (n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>n(((n((D=>n(A)))=>n((n((B=>n(D)))=>n(C))))=>n((n((n((B=>n(D)))=>n(C)))=>n((D=>n(A)))))))), poi_000550_bianassc, 1).
poi_theorem(an21, n(((n((n((A=>n(B)))=>n(C)))=>n((B=>n(n((A=>n(C)))))))=>n((n((B=>n(n((A=>n(C))))))=>n((n((A=>n(B)))=>n(C))))))), poi_000551_an21, 0.33).
poi_theorem(an12, n(((n((A=>n(n((B=>n(C))))))=>n((B=>n(n((A=>n(C)))))))=>n((n((B=>n(n((A=>n(C))))))=>n((A=>n(n((B=>n(C)))))))))), poi_000552_an12, 0.67).
poi_theorem(an32, n(((n((n((A=>n(B)))=>n(C)))=>n((n((A=>n(C)))=>n(B))))=>n((n((n((A=>n(C)))=>n(B)))=>n((n((A=>n(B)))=>n(C))))))), poi_000553_an32, 0.56).
poi_theorem(an13, n(((n((A=>n(n((B=>n(C))))))=>n((C=>n(n((B=>n(A)))))))=>n((n((C=>n(n((B=>n(A))))))=>n((A=>n(n((B=>n(C)))))))))), poi_000554_an13, 0.67).
poi_theorem(an31, n(((n((n((A=>n(B)))=>n(C)))=>n((n((C=>n(B)))=>n(A))))=>n((n((n((C=>n(B)))=>n(A)))=>n((n((A=>n(B)))=>n(C))))))), poi_000555_an31, 0.56).
poi_theorem(an12s, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((B=>n(n((A=>n(C))))))=>D)), poi_000556_an12s, 0.33).
poi_theorem(ancom2s, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(n((C=>n(B))))))=>D)), poi_000557_ancom2s, 0.22).
poi_theorem(an13s, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((C=>n(n((B=>n(A))))))=>D)), poi_000558_an13s, 0.44).
poi_theorem(an32s, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((A=>n(C)))=>n(B)))=>D)), poi_000559_an32s, 0.33).
poi_theorem(ancom1s, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((B=>n(A)))=>n(C)))=>D)), poi_000560_ancom1s, 0.22).
poi_theorem(an31s, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((C=>n(B)))=>n(A)))=>D)), poi_000561_an31s, 0.33).
poi_theorem(anass1rs, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((n((A=>n(C)))=>n(B)))=>D)), poi_000562_anass1rs, 0.44).
poi_theorem(an4, n(((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n((n((A=>n(C)))=>n(n((B=>n(D)))))))=>n((n((n((A=>n(C)))=>n(n((B=>n(D))))))=>n((n((A=>n(B)))=>n(n((C=>n(D)))))))))), poi_000563_an4, 0.89).
poi_theorem(an42, n(((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n((n((A=>n(C)))=>n(n((D=>n(B)))))))=>n((n((n((A=>n(C)))=>n(n((D=>n(B))))))=>n((n((A=>n(B)))=>n(n((C=>n(D)))))))))), poi_000564_an42, 0.89).
poi_theorem(an43, n(((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n((n((A=>n(D)))=>n(n((B=>n(C)))))))=>n((n((n((A=>n(D)))=>n(n((B=>n(C))))))=>n((n((A=>n(B)))=>n(n((C=>n(D)))))))))), poi_000565_an43, 0.89).
poi_theorem(an3, (n((n((A=>n(_)))=>n(n((_=>n(B))))))=>n((A=>n(B)))), poi_000566_an3, 0.11).
poi_theorem(an4s, ((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>E)=>(n((n((A=>n(C)))=>n(n((B=>n(D))))))=>E)), poi_000567_an4s, 0.89).
poi_theorem(an42s, ((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>E)=>(n((n((A=>n(C)))=>n(n((D=>n(B))))))=>E)), poi_000568_an42s, 0.89).
poi_theorem(anabs1, n(((n((n((A=>n(B)))=>n(A)))=>n((A=>n(B))))=>n((n((A=>n(B)))=>n((n((A=>n(B)))=>n(A))))))), poi_000569_anabs1, 0).
poi_theorem(anabs5, n(((n((A=>n(n((A=>n(B))))))=>n((A=>n(B))))=>n((n((A=>n(B)))=>n((A=>n(n((A=>n(B)))))))))), poi_000570_anabs5, 0).
poi_theorem(anabs7, n(((n((A=>n(n((B=>n(A))))))=>n((B=>n(A))))=>n((n((B=>n(A)))=>n((A=>n(n((B=>n(A)))))))))), poi_000571_anabs7, 0).
poi_theorem(anabsan, ((n((n((A=>n(A)))=>n(B)))=>C)=>(n((A=>n(B)))=>C)), poi_000572_anabsan, 0.11).
poi_theorem(anabss1, ((n((n((A=>n(B)))=>n(A)))=>C)=>(n((A=>n(B)))=>C)), poi_000573_anabss1, 0).
poi_theorem(anabss4, ((n((n((A=>n(B)))=>n(A)))=>C)=>(n((B=>n(A)))=>C)), poi_000574_anabss4, 0.11).
poi_theorem(anabss5, ((n((A=>n(n((A=>n(B))))))=>C)=>(n((A=>n(B)))=>C)), poi_000575_anabss5, 0).
poi_theorem(anabsi5, ((A=>(n((A=>n(B)))=>C))=>(n((A=>n(B)))=>C)), poi_000576_anabsi5, 0).
poi_theorem(anabsi6, ((A=>(n((B=>n(A)))=>C))=>(n((A=>n(B)))=>C)), poi_000577_anabsi6, 0.11).
poi_theorem(anabsi7, ((A=>(n((B=>n(A)))=>C))=>(n((B=>n(A)))=>C)), poi_000578_anabsi7, 0).
poi_theorem(anabsi8, ((A=>(n((A=>n(B)))=>C))=>(n((B=>n(A)))=>C)), poi_000579_anabsi8, 0.11).
poi_theorem(anabss7, ((n((A=>n(n((B=>n(A))))))=>C)=>(n((B=>n(A)))=>C)), poi_000580_anabss7, 0.11).
poi_theorem(anabsan2, ((n((A=>n(n((B=>n(B))))))=>C)=>(n((A=>n(B)))=>C)), poi_000581_anabsan2, 0.11).
poi_theorem(anabss3, ((n((n((A=>n(B)))=>n(B)))=>C)=>(n((A=>n(B)))=>C)), poi_000582_anabss3, 0).
poi_theorem(anandi, n(((n((A=>n(n((B=>n(C))))))=>n((n((A=>n(B)))=>n(n((A=>n(C)))))))=>n((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>n((A=>n(n((B=>n(C)))))))))), poi_000583_anandi, 0.67).
poi_theorem(anandir, n(((n((n((A=>n(B)))=>n(C)))=>n((n((A=>n(C)))=>n(n((B=>n(C)))))))=>n((n((n((A=>n(C)))=>n(n((B=>n(C))))))=>n((n((A=>n(B)))=>n(C))))))), poi_000584_anandir, 0.78).
poi_theorem(anandis, ((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>D)=>(n((A=>n(n((B=>n(C))))))=>D)), poi_000585_anandis, 0.44).
poi_theorem(anandirs, ((n((n((A=>n(B)))=>n(n((C=>n(B))))))=>D)=>(n((n((A=>n(C)))=>n(B)))=>D)), poi_000586_anandirs, 0.78).
poi_theorem(sylanl1, ((A=>B)=>((n((n((B=>n(C)))=>n(D)))=>E)=>(n((n((A=>n(C)))=>n(D)))=>E))), poi_000587_sylanl1, 1).
poi_theorem(sylanl2, ((A=>B)=>((n((n((C=>n(B)))=>n(D)))=>E)=>(n((n((C=>n(A)))=>n(D)))=>E))), poi_000588_sylanl2, 1).
poi_theorem(sylanr1, ((A=>B)=>((n((C=>n(n((B=>n(D))))))=>E)=>(n((C=>n(n((A=>n(D))))))=>E))), poi_000589_sylanr1, 1).
poi_theorem(sylanr2, ((A=>B)=>((n((C=>n(n((D=>n(B))))))=>E)=>(n((C=>n(n((D=>n(A))))))=>E))), poi_000590_sylanr2, 0.78).
poi_theorem(syl6an, ((A=>B)=>((A=>(C=>D))=>((n((B=>n(D)))=>E)=>(A=>(C=>E))))), poi_000591_syl6an, 0.78).
poi_theorem(syl2an2r, ((A=>B)=>((n((A=>n(C)))=>D)=>((n((B=>n(D)))=>E)=>(n((A=>n(C)))=>E)))), poi_000592_syl2an2r, 0.78).
poi_theorem(syl2an2, ((A=>B)=>((n((C=>n(A)))=>D)=>((n((B=>n(D)))=>E)=>(n((C=>n(A)))=>E)))), poi_000593_syl2an2, 1).
poi_theorem(mpdan, ((A=>B)=>((n((A=>n(B)))=>C)=>(A=>C))), poi_000594_mpdan, 0.11).
poi_theorem(mpancom, ((A=>B)=>((n((B=>n(A)))=>C)=>(A=>C))), poi_000595_mpancom, 0).
poi_theorem(mpidan, ((A=>B)=>((n((n((A=>n(C)))=>n(B)))=>D)=>(n((A=>n(C)))=>D))), poi_000596_mpidan, 0.67).
poi_theorem(mpan, (A=>((n((A=>n(B)))=>C)=>(B=>C))), poi_000597_mpan, 0.11).
poi_theorem(mpan2, (A=>((n((B=>n(A)))=>C)=>(B=>C))), poi_000598_mpan2, 0.11).
poi_theorem(mp2an, (A=>(B=>((n((A=>n(B)))=>C)=>C))), poi_000599_mp2an, 0.56).
poi_theorem(mp4an, (A=>(B=>(C=>(D=>((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>E)=>E))))), poi_000600_mp4an, 1).
poi_theorem(mpan2d, ((A=>B)=>((A=>(n((C=>n(B)))=>D))=>(A=>(C=>D)))), poi_000601_mpan2d, 0.89).
poi_theorem(mpand, ((A=>B)=>((A=>(n((B=>n(C)))=>D))=>(A=>(C=>D)))), poi_000602_mpand, 0.89).
poi_theorem(mpani, (A=>((B=>(n((A=>n(C)))=>D))=>(B=>(C=>D)))), poi_000603_mpani, 0.67).
poi_theorem(mpan2i, (A=>((B=>(n((C=>n(A)))=>D))=>(B=>(C=>D)))), poi_000604_mpan2i, 0.78).
poi_theorem(mp2ani, (A=>(B=>((C=>(n((A=>n(B)))=>D))=>(C=>D)))), poi_000605_mp2ani, 0.78).
poi_theorem(mp2and, ((A=>B)=>((A=>C)=>((A=>(n((B=>n(C)))=>D))=>(A=>D)))), poi_000606_mp2and, 1).
poi_theorem(mpanl1, (A=>((n((n((A=>n(B)))=>n(C)))=>D)=>(n((B=>n(C)))=>D))), poi_000607_mpanl1, 1).
poi_theorem(mpanl2, (A=>((n((n((B=>n(A)))=>n(C)))=>D)=>(n((B=>n(C)))=>D))), poi_000608_mpanl2, 1).
poi_theorem(mpanl12, (A=>(B=>((n((n((A=>n(B)))=>n(C)))=>D)=>(C=>D)))), poi_000609_mpanl12, 1).
poi_theorem(mpanr1, (A=>((n((B=>n(n((A=>n(C))))))=>D)=>(n((B=>n(C)))=>D))), poi_000610_mpanr1, 0.89).
poi_theorem(mpanr2, (A=>((n((B=>n(n((C=>n(A))))))=>D)=>(n((B=>n(C)))=>D))), poi_000611_mpanr2, 1).
poi_theorem(mpanr12, (A=>(B=>((n((C=>n(n((A=>n(B))))))=>D)=>(C=>D)))), poi_000612_mpanr12, 0.89).
poi_theorem(mpanlr1, (A=>((n((n((B=>n(n((A=>n(C))))))=>n(D)))=>E)=>(n((n((B=>n(C)))=>n(D)))=>E))), poi_000613_mpanlr1, 1).
poi_theorem(mpbirand, ((A=>B)=>((A=>n(((C=>n((B=>n(D))))=>n((n((B=>n(D)))=>C)))))=>(A=>n(((C=>D)=>n((D=>C))))))), poi_000614_mpbirand, 1).
poi_theorem(mpbiran2d, ((A=>B)=>((A=>n(((C=>n((D=>n(B))))=>n((n((D=>n(B)))=>C)))))=>(A=>n(((C=>D)=>n((D=>C))))))), poi_000615_mpbiran2d, 1).
poi_theorem(mpbiran, (A=>(n(((B=>n((A=>n(C))))=>n((n((A=>n(C)))=>B))))=>n(((B=>C)=>n((C=>B)))))), poi_000616_mpbiran, 1).
poi_theorem(mpbiran2, (A=>(n(((B=>n((C=>n(A))))=>n((n((C=>n(A)))=>B))))=>n(((B=>C)=>n((C=>B)))))), poi_000617_mpbiran2, 1).
poi_theorem(mpbir2an, (A=>(B=>(n(((C=>n((A=>n(B))))=>n((n((A=>n(B)))=>C))))=>C))), poi_000618_mpbir2an, 0.78).
poi_theorem(mpbi2and, ((A=>B)=>((A=>C)=>((A=>n(((n((B=>n(C)))=>D)=>n((D=>n((B=>n(C))))))))=>(A=>D)))), poi_000619_mpbi2and, 1).
poi_theorem(mpbir2and, ((A=>B)=>((A=>C)=>((A=>n(((D=>n((B=>n(C))))=>n((n((B=>n(C)))=>D)))))=>(A=>D)))), poi_000620_mpbir2and, 1).
poi_theorem(adantll, ((n((A=>n(B)))=>C)=>(n((n((_=>n(A)))=>n(B)))=>C)), poi_000621_adantll, 0).
poi_theorem(adantlr, ((n((A=>n(B)))=>C)=>(n((n((A=>n(_)))=>n(B)))=>C)), poi_000622_adantlr, 0).
poi_theorem(adantrl, ((n((A=>n(B)))=>C)=>(n((A=>n(n((_=>n(B))))))=>C)), poi_000623_adantrl, 0).
poi_theorem(adantrr, ((n((A=>n(B)))=>C)=>(n((A=>n(n((B=>n(_))))))=>C)), poi_000624_adantrr, 0).
poi_theorem(adantlll, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((_=>n(A)))=>n(B)))=>n(C)))=>D)), poi_000625_adantlll, 0.11).
poi_theorem(adantllr, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((A=>n(_)))=>n(B)))=>n(C)))=>D)), poi_000626_adantllr, 0).
poi_theorem(adantlrl, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((A=>n(n((_=>n(B))))))=>n(C)))=>D)), poi_000627_adantlrl, 0).
poi_theorem(adantlrr, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((A=>n(n((B=>n(_))))))=>n(C)))=>D)), poi_000628_adantlrr, 0).
poi_theorem(adantrll, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(n((n((_=>n(B)))=>n(C))))))=>D)), poi_000629_adantrll, 0.11).
poi_theorem(adantrlr, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(n((n((B=>n(_)))=>n(C))))))=>D)), poi_000630_adantrlr, 0).
poi_theorem(adantrrl, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(n((B=>n(n((_=>n(C)))))))))=>D)), poi_000631_adantrrl, 0).
poi_theorem(adantrrr, ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(n((B=>n(n((C=>n(_)))))))))=>D)), poi_000632_adantrrr, 0).
poi_theorem(ad2antrr, ((A=>B)=>(n((n((A=>n(_)))=>n(_)))=>B)), poi_000633_ad2antrr, 0.11).
poi_theorem(ad2antlr, ((A=>B)=>(n((n((_=>n(A)))=>n(_)))=>B)), poi_000634_ad2antlr, 0.11).
poi_theorem(ad2antrl, ((A=>B)=>(n((_=>n(n((A=>n(_))))))=>B)), poi_000635_ad2antrl, 0.11).
poi_theorem(ad2antll, ((A=>B)=>(n((_=>n(n((_=>n(A))))))=>B)), poi_000636_ad2antll, 0).
poi_theorem(ad3antrrr, ((A=>B)=>(n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000637_ad3antrrr, 0.11).
poi_theorem(ad3antlr, ((A=>B)=>(n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>B)), poi_000638_ad3antlr, 0.11).
poi_theorem(ad4antr, ((A=>B)=>(n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000639_ad4antr, 0).
poi_theorem(ad4antlr, ((A=>B)=>(n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000640_ad4antlr, 0.11).
poi_theorem(ad5antr, ((A=>B)=>(n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000641_ad5antr, 0.11).
poi_theorem(ad5antlr, ((A=>B)=>(n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000642_ad5antlr, 0.11).
poi_theorem(ad6antr, ((A=>B)=>(n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000643_ad6antr, 0.11).
poi_theorem(ad6antlr, ((A=>B)=>(n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000644_ad6antlr, 0.11).
poi_theorem(ad7antr, ((A=>B)=>(n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000645_ad7antr, 0.11).
poi_theorem(ad7antlr, ((A=>B)=>(n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000646_ad7antlr, 0.11).
poi_theorem(ad8antr, ((A=>B)=>(n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000647_ad8antr, 0.11).
poi_theorem(ad8antlr, ((A=>B)=>(n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000648_ad8antlr, 0.11).
poi_theorem(ad9antr, ((A=>B)=>(n((n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000649_ad9antr, 0.11).
poi_theorem(ad9antlr, ((A=>B)=>(n((n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000650_ad9antlr, 0.11).
poi_theorem(ad10antr, ((A=>B)=>(n((n((n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000651_ad10antr, 0.11).
poi_theorem(ad10antlr, ((A=>B)=>(n((n((n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>B)), poi_000652_ad10antlr, 0.11).
poi_theorem(ad2ant2l, ((n((A=>n(B)))=>C)=>(n((n((_=>n(A)))=>n(n((_=>n(B))))))=>C)), poi_000653_ad2ant2l, 0.11).
poi_theorem(ad2ant2r, ((n((A=>n(B)))=>C)=>(n((n((A=>n(_)))=>n(n((B=>n(_))))))=>C)), poi_000654_ad2ant2r, 0.11).
poi_theorem(ad2ant2lr, ((n((A=>n(B)))=>C)=>(n((n((_=>n(A)))=>n(n((B=>n(_))))))=>C)), poi_000655_ad2ant2lr, 0.11).
poi_theorem(ad2ant2rl, ((n((A=>n(B)))=>C)=>(n((n((A=>n(_)))=>n(n((_=>n(B))))))=>C)), poi_000656_ad2ant2rl, 0.11).
poi_theorem(adantl3r, ((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)=>(n((n((n((n((A=>n(_)))=>n(B)))=>n(C)))=>n(D)))=>E)), poi_000657_adantl3r, 0.11).
poi_theorem(ad4ant13, ((n((A=>n(B)))=>C)=>(n((n((n((A=>n(_)))=>n(B)))=>n(_)))=>C)), poi_000658_ad4ant13, 0.11).
poi_theorem(ad4ant14, ((n((A=>n(B)))=>C)=>(n((n((n((A=>n(_)))=>n(_)))=>n(B)))=>C)), poi_000659_ad4ant14, 0).
poi_theorem(ad4ant23, ((n((A=>n(B)))=>C)=>(n((n((n((_=>n(A)))=>n(B)))=>n(_)))=>C)), poi_000660_ad4ant23, 0.11).
poi_theorem(ad4ant24, ((n((A=>n(B)))=>C)=>(n((n((n((_=>n(A)))=>n(_)))=>n(B)))=>C)), poi_000661_ad4ant24, 0).
poi_theorem(adantl4r, ((n((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>n(E)))=>F)=>(n((n((n((n((n((A=>n(_)))=>n(B)))=>n(C)))=>n(D)))=>n(E)))=>F)), poi_000662_adantl4r, 0.56).
poi_theorem(ad5ant12, ((n((A=>n(B)))=>C)=>(n((n((n((n((A=>n(B)))=>n(_)))=>n(_)))=>n(_)))=>C)), poi_000663_ad5ant12, 0).
poi_theorem(ad5ant13, ((n((A=>n(B)))=>C)=>(n((n((n((n((A=>n(_)))=>n(B)))=>n(_)))=>n(_)))=>C)), poi_000664_ad5ant13, 0).
poi_theorem(ad5ant14, ((n((A=>n(B)))=>C)=>(n((n((n((n((A=>n(_)))=>n(_)))=>n(B)))=>n(_)))=>C)), poi_000665_ad5ant14, 0).
poi_theorem(ad5ant15, ((n((A=>n(B)))=>C)=>(n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(B)))=>C)), poi_000666_ad5ant15, 0.11).
poi_theorem(ad5ant23, ((n((A=>n(B)))=>C)=>(n((n((n((n((_=>n(A)))=>n(B)))=>n(_)))=>n(_)))=>C)), poi_000667_ad5ant23, 0).
poi_theorem(ad5ant24, ((n((A=>n(B)))=>C)=>(n((n((n((n((_=>n(A)))=>n(_)))=>n(B)))=>n(_)))=>C)), poi_000668_ad5ant24, 0).
poi_theorem(ad5ant25, ((n((A=>n(B)))=>C)=>(n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(B)))=>C)), poi_000669_ad5ant25, 0.11).
poi_theorem(adantl5r, ((n((n((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>n(E)))=>n(F)))=>G)=>(n((n((n((n((n((n((A=>n(_)))=>n(B)))=>n(C)))=>n(D)))=>n(E)))=>n(F)))=>G)), poi_000670_adantl5r, 0.78).
poi_theorem(adantl6r, ((n((n((n((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>n(E)))=>n(F)))=>n(G)))=>H)=>(n((n((n((n((n((n((n((A=>n(_)))=>n(B)))=>n(C)))=>n(D)))=>n(E)))=>n(F)))=>n(G)))=>H)), poi_000671_adantl6r, 0.78).
poi_theorem('pm3.33', (n(((A=>B)=>n((B=>C))))=>(A=>C)), 'poi_000672_pm3.33', 0.11).
poi_theorem('pm3.34', (n(((A=>B)=>n((C=>A))))=>(C=>B)), 'poi_000673_pm3.34', 0).
poi_theorem(simpll, (n((n((A=>n(_)))=>n(_)))=>A), poi_000674_simpll, 0).
poi_theorem(simplld, ((A=>n((n((B=>n(_)))=>n(_))))=>(A=>B)), poi_000675_simplld, 0).
poi_theorem(simplr, (n((n((_=>n(A)))=>n(_)))=>A), poi_000676_simplr, 0).
poi_theorem(simplrd, ((A=>n((n((_=>n(B)))=>n(_))))=>(A=>B)), poi_000677_simplrd, 0).
poi_theorem(simprl, (n((_=>n(n((A=>n(_))))))=>A), poi_000678_simprl, 0).
poi_theorem(simprld, ((A=>n((_=>n(n((B=>n(_)))))))=>(A=>B)), poi_000679_simprld, 0).
poi_theorem(simprr, (n((_=>n(n((_=>n(A))))))=>A), poi_000680_simprr, 0).
poi_theorem(simprrd, ((A=>n((_=>n(n((_=>n(B)))))))=>(A=>B)), poi_000681_simprrd, 0).
poi_theorem(simplll, (n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>A), poi_000682_simplll, 0).
poi_theorem(simpllr, (n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>A), poi_000683_simpllr, 0).
poi_theorem(simplrl, (n((n((_=>n(n((A=>n(_))))))=>n(_)))=>A), poi_000684_simplrl, 0).
poi_theorem(simplrr, (n((n((_=>n(n((_=>n(A))))))=>n(_)))=>A), poi_000685_simplrr, 0).
poi_theorem(simprll, (n((_=>n(n((n((A=>n(_)))=>n(_))))))=>A), poi_000686_simprll, 0).
poi_theorem(simprlr, (n((_=>n(n((n((_=>n(A)))=>n(_))))))=>A), poi_000687_simprlr, 0).
poi_theorem(simprrl, (n((_=>n(n((_=>n(n((A=>n(_)))))))))=>A), poi_000688_simprrl, 0).
poi_theorem(simprrr, (n((_=>n(n((_=>n(n((_=>n(A)))))))))=>A), poi_000689_simprrr, 0).
poi_theorem('simp-4l', (n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000690_simp-4l', 0).
poi_theorem('simp-4r', (n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000691_simp-4r', 0).
poi_theorem('simp-5l', (n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000692_simp-5l', 0).
poi_theorem('simp-5r', (n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000693_simp-5r', 0).
poi_theorem('simp-6l', (n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000694_simp-6l', 0).
poi_theorem('simp-6r', (n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000695_simp-6r', 0).
poi_theorem('simp-7l', (n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000696_simp-7l', 0).
poi_theorem('simp-7r', (n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000697_simp-7r', 0).
poi_theorem('simp-8l', (n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000698_simp-8l', 0).
poi_theorem('simp-8r', (n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000699_simp-8r', 0).
poi_theorem('simp-9l', (n((n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000700_simp-9l', 0).
poi_theorem('simp-9r', (n((n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000701_simp-9r', 0).
poi_theorem('simp-10l', (n((n((n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000702_simp-10l', 0).
poi_theorem('simp-10r', (n((n((n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000703_simp-10r', 0).
poi_theorem('simp-11l', (n((n((n((n((n((n((n((n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000704_simp-11l', 0).
poi_theorem('simp-11r', (n((n((n((n((n((n((n((n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), 'poi_000705_simp-11r', 0).
poi_theorem('pm2.01da', ((n((A=>n(B)))=>n(B))=>(A=>n(B))), 'poi_000706_pm2.01da', 0).
poi_theorem('pm2.18da', ((n((A=>n(n(B))))=>B)=>(A=>B)), 'poi_000707_pm2.18da', 0).
poi_theorem(impbida, ((n((A=>n(B)))=>C)=>((n((A=>n(C)))=>B)=>(A=>n(((B=>C)=>n((C=>B))))))), poi_000708_impbida, 1).
poi_theorem('pm5.21nd', ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>C)=>((C=>n(((B=>D)=>n((D=>B)))))=>(A=>n(((B=>D)=>n((D=>B)))))))), 'poi_000709_pm5.21nd', 1).
poi_theorem('pm3.35', (n((A=>n((A=>B))))=>B), 'poi_000710_pm3.35', 0).
poi_theorem('pm5.74da', ((n((A=>n(B)))=>n(((C=>D)=>n((D=>C)))))=>(A=>n((((B=>C)=>(B=>D))=>n(((B=>D)=>(B=>C))))))), 'poi_000711_pm5.74da', 1).
poi_theorem(bitr, (n((n(((A=>B)=>n((B=>A))))=>n(n(((B=>C)=>n((C=>B)))))))=>n(((A=>C)=>n((C=>A))))), poi_000712_bitr, 1).
poi_theorem(biantr, (n((n(((A=>B)=>n((B=>A))))=>n(n(((C=>B)=>n((B=>C)))))))=>n(((A=>C)=>n((C=>A))))), poi_000713_biantr, 1).
poi_theorem('pm4.14', n((((n((A=>n(B)))=>C)=>(n((A=>n(n(C))))=>n(B)))=>n(((n((A=>n(n(C))))=>n(B))=>(n((A=>n(B)))=>C))))), 'poi_000714_pm4.14', 0.33).
poi_theorem('pm3.37', ((n((A=>n(B)))=>C)=>(n((A=>n(n(C))))=>n(B))), 'poi_000715_pm3.37', 0.11).
poi_theorem(anim12, (n(((A=>B)=>n((C=>D))))=>(n((A=>n(C)))=>n((B=>n(D))))), poi_000716_anim12, 0.67).
poi_theorem('pm3.4', (n((A=>n(B)))=>(A=>B)), 'poi_000717_pm3.4', 0).
poi_theorem(exbiri, ((n((A=>n(B)))=>n(((C=>D)=>n((D=>C)))))=>(A=>(B=>(D=>C)))), poi_000718_exbiri, 0.33).
poi_theorem('pm2.61ian', ((n((A=>n(B)))=>C)=>((n((n(A)=>n(B)))=>C)=>(B=>C))), 'poi_000719_pm2.61ian', 0.11).
poi_theorem('pm2.61dan', ((n((A=>n(B)))=>C)=>((n((A=>n(n(B))))=>C)=>(A=>C))), 'poi_000720_pm2.61dan', 0.22).
poi_theorem('pm2.61ddan', ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>C)=>((n((A=>n(n((n(B)=>n(n(D)))))))=>C)=>(A=>C)))), 'poi_000721_pm2.61ddan', 1).
poi_theorem('pm2.61dda', ((n((A=>n(n(B))))=>C)=>((n((A=>n(n(D))))=>C)=>((n((A=>n(n((B=>n(D))))))=>C)=>(A=>C)))), 'poi_000722_pm2.61dda', 1).
poi_theorem(mtand, ((A=>n(B))=>((n((A=>n(C)))=>B)=>(A=>n(C)))), poi_000723_mtand, 0.11).
poi_theorem('pm2.65da', ((n((A=>n(B)))=>C)=>((n((A=>n(B)))=>n(C))=>(A=>n(B)))), 'poi_000724_pm2.65da', 0.22).
poi_theorem(condan, ((n((A=>n(n(B))))=>C)=>((n((A=>n(n(B))))=>n(C))=>(A=>B))), poi_000725_condan, 0.44).
poi_theorem(biadan, n((((A=>B)=>n((((B=>n(((A=>C)=>n((C=>A)))))=>n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A)))))=>n((n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(B=>n(((A=>C)=>n((C=>A))))))))))=>n((n((((B=>n(((A=>C)=>n((C=>A)))))=>n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A)))))=>n((n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(B=>n(((A=>C)=>n((C=>A)))))))))=>(A=>B))))), poi_000726_biadan, 1).
poi_theorem(biadani, ((A=>B)=>n((((B=>n(((A=>C)=>n((C=>A)))))=>n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A)))))=>n((n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A))))=>(B=>n(((A=>C)=>n((C=>A)))))))))), poi_000727_biadani, 1).
poi_theorem(biadanii, ((A=>B)=>((B=>n(((A=>C)=>n((C=>A)))))=>n(((A=>n((B=>n(C))))=>n((n((B=>n(C)))=>A)))))), poi_000728_biadanii, 1).
poi_theorem(biadanid, ((n((A=>n(B)))=>C)=>((n((A=>n(C)))=>n(((B=>D)=>n((D=>B)))))=>(A=>n(((B=>n((C=>n(D))))=>n((n((C=>n(D)))=>B))))))), poi_000729_biadanid, 1).
poi_theorem('pm5.1', (n((A=>n(B)))=>n(((A=>B)=>n((B=>A))))), 'poi_000730_pm5.1', 0.11).
poi_theorem('pm5.21', (n((n(A)=>n(n(B))))=>n(((A=>B)=>n((B=>A))))), 'poi_000731_pm5.21', 0.11).
poi_theorem('pm5.35', (n(((A=>B)=>n((A=>C))))=>(A=>n(((B=>C)=>n((C=>B)))))), 'poi_000732_pm5.35', 0.78).
poi_theorem(abai, n(((n((A=>n(B)))=>n((A=>n((A=>B)))))=>n((n((A=>n((A=>B))))=>n((A=>n(B))))))), poi_000733_abai, 0.11).
poi_theorem('pm4.45im', n(((A=>n((A=>n((B=>A)))))=>n((n((A=>n((B=>A))))=>A)))), 'poi_000734_pm4.45im', 0).
poi_theorem(impimprbi, n(((n(((A=>B)=>n((B=>A))))=>n((((A=>B)=>(B=>A))=>n(((B=>A)=>(A=>B))))))=>n((n((((A=>B)=>(B=>A))=>n(((B=>A)=>(A=>B)))))=>n(((A=>B)=>n((B=>A)))))))), poi_000735_impimprbi, 0.67).
poi_theorem(nan, n((((A=>n(n((B=>n(C)))))=>(n((A=>n(B)))=>n(C)))=>n(((n((A=>n(B)))=>n(C))=>(A=>n(n((B=>n(C))))))))), poi_000736_nan, 0.33).
poi_theorem('pm5.31', (n((A=>n((B=>C))))=>(B=>n((C=>n(A))))), 'poi_000737_pm5.31', 0.33).
poi_theorem('pm5.31r', (n((A=>n((B=>C))))=>(B=>n((A=>n(C))))), 'poi_000738_pm5.31r', 0.33).
poi_theorem('pm4.15', n((((n((A=>n(B)))=>n(C))=>(n((B=>n(C)))=>n(A)))=>n(((n((B=>n(C)))=>n(A))=>(n((A=>n(B)))=>n(C)))))), 'poi_000739_pm4.15', 0.33).
poi_theorem('pm5.36', n(((n((A=>n(n(((A=>B)=>n((B=>A)))))))=>n((B=>n(n(((A=>B)=>n((B=>A))))))))=>n((n((B=>n(n(((A=>B)=>n((B=>A)))))))=>n((A=>n(n(((A=>B)=>n((B=>A))))))))))), 'poi_000740_pm5.36', 0.67).
poi_theorem(annotanannot, n(((n((A=>n(n(n((A=>n(B)))))))=>n((A=>n(n(B)))))=>n((n((A=>n(n(B))))=>n((A=>n(n(n((A=>n(B))))))))))), poi_000741_annotanannot, 0.11).
poi_theorem('pm5.33', n(((n((A=>n((B=>C))))=>n((A=>n((n((A=>n(B)))=>C)))))=>n((n((A=>n((n((A=>n(B)))=>C))))=>n((A=>n((B=>C)))))))), 'poi_000742_pm5.33', 0.56).
poi_theorem(syl12anc, ((A=>B)=>((A=>C)=>((A=>D)=>((n((B=>n(n((C=>n(D))))))=>E)=>(A=>E))))), poi_000743_syl12anc, 0.78).
poi_theorem(syl21anc, ((A=>B)=>((A=>C)=>((A=>D)=>((n((n((B=>n(C)))=>n(D)))=>E)=>(A=>E))))), poi_000744_syl21anc, 1).
poi_theorem(syl22anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((n((n((B=>n(C)))=>n(n((D=>n(E))))))=>F)=>(A=>F)))))), poi_000745_syl22anc, 1).
poi_theorem(syl1111anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((n((n((n((B=>n(C)))=>n(D)))=>n(E)))=>F)=>(A=>F)))))), poi_000746_syl1111anc, 1).
poi_theorem(syldbl2, ((n((A=>n(B)))=>(B=>C))=>(n((A=>n(B)))=>C)), poi_000747_syldbl2, 0).
poi_theorem(mpsyl4anc, (A=>(B=>(C=>((D=>E)=>((n((n((n((A=>n(B)))=>n(C)))=>n(E)))=>F)=>(D=>F)))))), poi_000748_mpsyl4anc, 1).
poi_theorem('pm4.87', n((n((n((((n((A=>n(B)))=>C)=>(A=>(B=>C)))=>n(((A=>(B=>C))=>(n((A=>n(B)))=>C)))))=>n(n((((A=>(B=>C))=>(B=>(A=>C)))=>n(((B=>(A=>C))=>(A=>(B=>C)))))))))=>n(n((((B=>(A=>C))=>(n((B=>n(A)))=>C))=>n(((n((B=>n(A)))=>C)=>(B=>(A=>C))))))))), 'poi_000749_pm4.87', 0.78).
poi_theorem(bimsc1, (n(((A=>B)=>n(n(((C=>n((B=>n(A))))=>n((n((B=>n(A)))=>C)))))))=>n(((C=>A)=>n((A=>C))))), poi_000750_bimsc1, 1).
poi_theorem(a2and, ((A=>(n((B=>n(C)))=>(D=>E)))=>((A=>(n((B=>n(C)))=>F))=>(A=>((n((B=>n(F)))=>D)=>(n((B=>n(C)))=>E))))), poi_000751_a2and, 1).
poi_theorem(animpimp2impd, ((n((A=>n(B)))=>(C=>(D=>E)))=>((n((A=>n(n((B=>n(D))))))=>(E=>F))=>(B=>((A=>C)=>(A=>(D=>F)))))), poi_000752_animpimp2impd, 1).
poi_theorem('pm4.64', n((((n(A)=>B)=>(n(A)=>B))=>n(((n(A)=>B)=>(n(A)=>B))))), 'poi_000753_pm4.64', 0).
poi_theorem('pm4.66', n((((n(A)=>n(B))=>(n(A)=>n(B)))=>n(((n(A)=>n(B))=>(n(A)=>n(B)))))), 'poi_000754_pm4.66', 0).
poi_theorem('pm2.53', ((n(A)=>B)=>(n(A)=>B)), 'poi_000755_pm2.53', 0).
poi_theorem(imor, n((((A=>B)=>(n(n(A))=>B))=>n(((n(n(A))=>B)=>(A=>B))))), poi_000756_imor, 0).
poi_theorem(imorri, ((n(n(A))=>B)=>(A=>B)), poi_000757_imorri, 0).
poi_theorem('pm4.62', n((((A=>n(B))=>(n(n(A))=>n(B)))=>n(((n(n(A))=>n(B))=>(A=>n(B)))))), 'poi_000758_pm4.62', 0).
poi_theorem(jao1i, ((A=>(B=>C))=>((n(C)=>A)=>(B=>C))), poi_000759_jao1i, 0.11).
poi_theorem(jaod, ((A=>(B=>C))=>((A=>(D=>C))=>(A=>((n(B)=>D)=>C)))), poi_000760_jaod, 0.89).
poi_theorem(mpjaod, ((A=>(B=>C))=>((A=>(D=>C))=>((A=>(n(B)=>D))=>(A=>C)))), poi_000761_mpjaod, 0.89).
poi_theorem(orrd, ((A=>(n(B)=>C))=>(A=>(n(B)=>C))), poi_000762_orrd, 0).
poi_theorem(olc, (A=>(n(_)=>A)), poi_000763_olc, 0).
poi_theorem(orcoms, (((n(A)=>B)=>C)=>((n(B)=>A)=>C)), poi_000764_orcoms, 0).
poi_theorem(olcd, ((A=>B)=>(A=>(n(_)=>B))), poi_000765_olcd, 0).
poi_theorem(olcs, (((n(_)=>A)=>B)=>(A=>B)), poi_000766_olcs, 0).
poi_theorem(olcnd, ((A=>(n(B)=>C))=>((A=>n(C))=>(A=>B))), poi_000767_olcnd, 0).
poi_theorem(orcnd, ((A=>(n(B)=>C))=>((A=>n(B))=>(A=>C))), poi_000768_orcnd, 0).
poi_theorem(mtord, ((A=>n(B))=>((A=>n(C))=>((A=>(D=>(n(B)=>C)))=>(A=>n(D))))), poi_000769_mtord, 0.78).
poi_theorem('pm3.2ni', (n(A)=>(n(B)=>n((n(A)=>B)))), 'poi_000770_pm3.2ni', 0).
poi_theorem('pm2.45', (n((n(A)=>_))=>n(A)), 'poi_000771_pm2.45', 0).
poi_theorem('pm2.46', (n((n(_)=>A))=>n(A)), 'poi_000772_pm2.46', 0).
poi_theorem('pm2.47', (n((n(A)=>B))=>(n(n(A))=>B)), 'poi_000773_pm2.47', 0).
poi_theorem('pm2.48', (n((n(A)=>B))=>(n(A)=>n(B))), 'poi_000774_pm2.48', 0).
poi_theorem('pm2.49', (n((n(A)=>B))=>(n(n(A))=>n(B))), 'poi_000775_pm2.49', 0).
poi_theorem(norbi, (n((n(A)=>B))=>n(((A=>B)=>n((B=>A))))), poi_000776_norbi, 0.11).
poi_theorem(nbior, (n(n(((A=>B)=>n((B=>A)))))=>(n(A)=>B)), poi_000777_nbior, 0.11).
poi_theorem(orel1, (n(A)=>((n(A)=>B)=>B)), poi_000778_orel1, 0).
poi_theorem(orel2, (n(A)=>((n(B)=>A)=>B)), poi_000779_orel2, 0).
poi_theorem('pm2.67-2', (((n(A)=>_)=>B)=>(A=>B)), 'poi_000780_pm2.67-2', 0).
poi_theorem('pm2.67', (((n(A)=>B)=>B)=>(A=>B)), 'poi_000781_pm2.67', 0).
poi_theorem(exmid, (n(A)=>n(A)), poi_000782_exmid, 0).
poi_theorem(exmidd, (_=>(n(A)=>n(A))), poi_000783_exmidd, 0).
poi_theorem('pm2.13', (n(A)=>n(n(n(A)))), 'poi_000784_pm2.13', 0).
poi_theorem('pm2.68', (((A=>B)=>B)=>(n(A)=>B)), 'poi_000785_pm2.68', 0).
poi_theorem(dfor2, n((((n(A)=>B)=>((A=>B)=>B))=>n((((A=>B)=>B)=>(n(A)=>B))))), poi_000786_dfor2, 0).
poi_theorem('pm2.07', (A=>(n(A)=>A)), 'poi_000787_pm2.07', 0).
poi_theorem('pm4.25', n(((A=>(n(A)=>A))=>n(((n(A)=>A)=>A)))), 'poi_000788_pm4.25', 0).
poi_theorem('pm2.4', ((n(A)=>(n(A)=>B))=>(n(A)=>B)), 'poi_000789_pm2.4', 0).
poi_theorem('pm2.41', ((n(A)=>(n(B)=>A))=>(n(B)=>A)), 'poi_000790_pm2.41', 0).
poi_theorem(orim12i, ((A=>B)=>((C=>D)=>((n(A)=>C)=>(n(B)=>D)))), poi_000791_orim12i, 0.33).
poi_theorem(orim12dALT, ((A=>(B=>C))=>((A=>(D=>E))=>(A=>((n(B)=>D)=>(n(C)=>E))))), poi_000792_orim12dALT, 1).
poi_theorem(orbi2i, (n(((A=>B)=>n((B=>A))))=>n((((n(C)=>A)=>(n(C)=>B))=>n(((n(C)=>B)=>(n(C)=>A)))))), poi_000793_orbi2i, 0.56).
poi_theorem(orbi12i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n((((n(A)=>C)=>(n(B)=>D))=>n(((n(B)=>D)=>(n(A)=>C))))))), poi_000794_orbi12i, 1).
poi_theorem(orbi2d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n((((n(D)=>B)=>(n(D)=>C))=>n(((n(D)=>C)=>(n(D)=>B))))))), poi_000795_orbi2d, 0.56).
poi_theorem(orbi1d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n((((n(B)=>D)=>(n(C)=>D))=>n(((n(C)=>D)=>(n(B)=>D))))))), poi_000796_orbi1d, 1).
poi_theorem(orbi1, (n(((A=>B)=>n((B=>A))))=>n((((n(A)=>C)=>(n(B)=>C))=>n(((n(B)=>C)=>(n(A)=>C)))))), poi_000797_orbi1, 1).
poi_theorem(orbi12d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n((((n(B)=>D)=>(n(C)=>E))=>n(((n(C)=>E)=>(n(B)=>D)))))))), poi_000798_orbi12d, 1).
poi_theorem('pm1.5', ((n(A)=>(n(B)=>C))=>(n(B)=>(n(A)=>C))), 'poi_000799_pm1.5', 0).
poi_theorem(or12, n((((n(A)=>(n(B)=>C))=>(n(B)=>(n(A)=>C)))=>n(((n(B)=>(n(A)=>C))=>(n(A)=>(n(B)=>C)))))), poi_000800_or12, 0).
poi_theorem(orass, n((((n((n(A)=>B))=>C)=>(n(A)=>(n(B)=>C)))=>n(((n(A)=>(n(B)=>C))=>(n((n(A)=>B))=>C))))), poi_000801_orass, 0.33).
poi_theorem('pm2.31', ((n(A)=>(n(B)=>C))=>(n((n(A)=>B))=>C)), 'poi_000802_pm2.31', 0).
poi_theorem('pm2.32', ((n((n(A)=>B))=>C)=>(n(A)=>(n(B)=>C))), 'poi_000803_pm2.32', 0.11).
poi_theorem('pm2.3', ((n(A)=>(n(B)=>C))=>(n(A)=>(n(C)=>B))), 'poi_000804_pm2.3', 0).
poi_theorem(or32, n((((n((n(A)=>B))=>C)=>(n((n(A)=>C))=>B))=>n(((n((n(A)=>C))=>B)=>(n((n(A)=>B))=>C))))), poi_000805_or32, 0.33).
poi_theorem(or4, n((((n((n(A)=>B))=>(n(C)=>D))=>(n((n(A)=>C))=>(n(B)=>D)))=>n(((n((n(A)=>C))=>(n(B)=>D))=>(n((n(A)=>B))=>(n(C)=>D)))))), poi_000806_or4, 0.78).
poi_theorem(or42, n((((n((n(A)=>B))=>(n(C)=>D))=>(n((n(A)=>C))=>(n(D)=>B)))=>n(((n((n(A)=>C))=>(n(D)=>B))=>(n((n(A)=>B))=>(n(C)=>D)))))), poi_000807_or42, 0.78).
poi_theorem(orordi, n((((n(A)=>(n(B)=>C))=>(n((n(A)=>B))=>(n(A)=>C)))=>n(((n((n(A)=>B))=>(n(A)=>C))=>(n(A)=>(n(B)=>C)))))), poi_000808_orordi, 0.56).
poi_theorem(orordir, n((((n((n(A)=>B))=>C)=>(n((n(A)=>C))=>(n(B)=>C)))=>n(((n((n(A)=>C))=>(n(B)=>C))=>(n((n(A)=>B))=>C))))), poi_000809_orordir, 0.33).
poi_theorem(orimdi, n((((n(A)=>(B=>C))=>((n(A)=>B)=>(n(A)=>C)))=>n((((n(A)=>B)=>(n(A)=>C))=>(n(A)=>(B=>C)))))), poi_000810_orimdi, 0).
poi_theorem('pm2.76', ((n(A)=>(B=>C))=>((n(A)=>B)=>(n(A)=>C))), 'poi_000811_pm2.76', 0).
poi_theorem('pm2.85', (((n(A)=>B)=>(n(A)=>C))=>(n(A)=>(B=>C))), 'poi_000812_pm2.85', 0.11).
poi_theorem('pm2.75', ((n(A)=>B)=>((n(A)=>(B=>C))=>(n(A)=>C))), 'poi_000813_pm2.75', 0).
poi_theorem('pm4.78', n((((n((A=>B))=>(A=>C))=>(A=>(n(B)=>C)))=>n(((A=>(n(B)=>C))=>(n((A=>B))=>(A=>C)))))), 'poi_000814_pm4.78', 0.11).
poi_theorem(biort, (A=>n(((A=>(n(A)=>B))=>n(((n(A)=>B)=>A))))), poi_000815_biort, 0).
poi_theorem(biorf, (n(A)=>n(((B=>(n(A)=>B))=>n(((n(A)=>B)=>B))))), poi_000816_biorf, 0).
poi_theorem(biortn, (A=>n(((B=>(n(n(A))=>B))=>n(((n(n(A))=>B)=>B))))), poi_000817_biortn, 0).
poi_theorem(biorfi, (n(A)=>n(((B=>(n(B)=>A))=>n(((n(B)=>A)=>B))))), poi_000818_biorfi, 0.11).
poi_theorem('pm2.26', (n(n(A))=>((A=>B)=>B)), 'poi_000819_pm2.26', 0).
poi_theorem('pm2.63', ((n(A)=>B)=>((n(n(A))=>B)=>B)), 'poi_000820_pm2.63', 0.11).
poi_theorem('pm2.64', ((n(A)=>B)=>((n(A)=>n(B))=>A)), 'poi_000821_pm2.64', 0).
poi_theorem('pm2.42', ((n(n(A))=>(A=>B))=>(A=>B)), 'poi_000822_pm2.42', 0).
poi_theorem('pm5.55', (n(n((((n(A)=>B)=>A)=>n((A=>(n(A)=>B))))))=>n((((n(A)=>B)=>B)=>n((B=>(n(A)=>B)))))), 'poi_000823_pm5.55', 0.11).
poi_theorem('pm4.72', n((((A=>B)=>n(((B=>(n(A)=>B))=>n(((n(A)=>B)=>B)))))=>n((n(((B=>(n(A)=>B))=>n(((n(A)=>B)=>B))))=>(A=>B))))), 'poi_000824_pm4.72', 0.11).
poi_theorem(imimorb, n(((((A=>B)=>(C=>B))=>(C=>(n(A)=>B)))=>n(((C=>(n(A)=>B))=>((A=>B)=>(C=>B)))))), poi_000825_imimorb, 0.11).
poi_theorem(oibabs, n(((((n(A)=>B)=>n(((A=>B)=>n((B=>A)))))=>n(((A=>B)=>n((B=>A)))))=>n((n(((A=>B)=>n((B=>A))))=>((n(A)=>B)=>n(((A=>B)=>n((B=>A))))))))), poi_000826_oibabs, 0).
poi_theorem(orbidi, n((((n(A)=>n(((B=>C)=>n((C=>B)))))=>n((((n(A)=>B)=>(n(A)=>C))=>n(((n(A)=>C)=>(n(A)=>B))))))=>n((n((((n(A)=>B)=>(n(A)=>C))=>n(((n(A)=>C)=>(n(A)=>B)))))=>(n(A)=>n(((B=>C)=>n((C=>B))))))))), poi_000827_orbidi, 1).
poi_theorem('pm5.7', n(((n((((n(A)=>B)=>(n(C)=>B))=>n(((n(C)=>B)=>(n(A)=>B)))))=>(n(B)=>n(((A=>C)=>n((C=>A))))))=>n(((n(B)=>n(((A=>C)=>n((C=>A)))))=>n((((n(A)=>B)=>(n(C)=>B))=>n(((n(C)=>B)=>(n(A)=>B))))))))), 'poi_000828_pm5.7', 1).
poi_theorem(jaao, ((A=>(B=>C))=>((D=>(E=>C))=>(n((A=>n(D)))=>((n(B)=>E)=>C)))), poi_000829_jaao, 1).
poi_theorem(jaoa, ((A=>(B=>C))=>((D=>(E=>C))=>((n(A)=>D)=>(n((B=>n(E)))=>C)))), poi_000830_jaoa, 1).
poi_theorem(jaoian, ((n((A=>n(B)))=>C)=>((n((D=>n(B)))=>C)=>(n(((n(A)=>D)=>n(B)))=>C))), poi_000831_jaoian, 0.89).
poi_theorem(jaodan, ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>C)=>(n((A=>n((n(B)=>D))))=>C))), poi_000832_jaodan, 1).
poi_theorem(mpjaodan, ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>C)=>((A=>(n(B)=>D))=>(A=>C)))), poi_000833_mpjaodan, 1).
poi_theorem('pm3.44', (n(((A=>B)=>n((C=>B))))=>((n(A)=>C)=>B)), 'poi_000834_pm3.44', 0.11).
poi_theorem(jao, ((A=>B)=>((C=>B)=>((n(A)=>C)=>B))), poi_000835_jao, 0.11).
poi_theorem(jaob, n(((((n(A)=>B)=>C)=>n(((A=>C)=>n((B=>C)))))=>n((n(((A=>C)=>n((B=>C))))=>((n(A)=>B)=>C))))), poi_000836_jaob, 0.33).
poi_theorem('pm4.77', n(((n(((A=>B)=>n((C=>B))))=>((n(A)=>C)=>B))=>n((((n(A)=>C)=>B)=>n(((A=>B)=>n((C=>B)))))))), 'poi_000837_pm4.77', 0.33).
poi_theorem('pm3.48', (n(((A=>B)=>n((C=>D))))=>((n(A)=>C)=>(n(B)=>D))), 'poi_000838_pm3.48', 0.56).
poi_theorem(orim1d, ((A=>(B=>C))=>(A=>((n(B)=>D)=>(n(C)=>D)))), poi_000839_orim1d, 0.11).
poi_theorem(orim2d, ((A=>(B=>C))=>(A=>((n(D)=>B)=>(n(D)=>C)))), poi_000840_orim2d, 0).
poi_theorem(orim2, ((A=>B)=>((n(C)=>A)=>(n(C)=>B))), poi_000841_orim2, 0).
poi_theorem('pm2.38', ((A=>B)=>((n(A)=>C)=>(n(B)=>C))), 'poi_000842_pm2.38', 0.11).
poi_theorem('pm2.36', ((A=>B)=>((n(C)=>A)=>(n(B)=>C))), 'poi_000843_pm2.36', 0).
poi_theorem('pm2.37', ((A=>B)=>((n(A)=>C)=>(n(C)=>B))), 'poi_000844_pm2.37', 0).
poi_theorem('pm2.81', ((A=>(B=>C))=>((n(D)=>A)=>((n(D)=>B)=>(n(D)=>C)))), 'poi_000845_pm2.81', 0.44).
poi_theorem('pm2.8', ((n(A)=>B)=>((n(n(B))=>C)=>(n(A)=>C))), 'poi_000846_pm2.8', 0).
poi_theorem('pm2.73', ((A=>B)=>((n((n(A)=>B))=>C)=>(n(B)=>C))), 'poi_000847_pm2.73', 0.22).
poi_theorem('pm2.74', ((A=>B)=>((n((n(B)=>A))=>C)=>(n(B)=>C))), 'poi_000848_pm2.74', 0.11).
poi_theorem('pm2.82', ((n((n(A)=>B))=>C)=>((n((n(A)=>n(C)))=>D)=>(n((n(A)=>B))=>D))), 'poi_000849_pm2.82', 0.78).
poi_theorem('pm4.39', (n((n(((A=>B)=>n((B=>A))))=>n(n(((C=>D)=>n((D=>C)))))))=>n((((n(A)=>C)=>(n(B)=>D))=>n(((n(B)=>D)=>(n(A)=>C)))))), 'poi_000850_pm4.39', 1).
poi_theorem(animorl, (n((A=>n(_)))=>(n(A)=>_)), poi_000851_animorl, 0).
poi_theorem(animorr, (n((_=>n(A)))=>(n(_)=>A)), poi_000852_animorr, 0).
poi_theorem(animorlr, (n((A=>n(_)))=>(n(_)=>A)), poi_000853_animorlr, 0).
poi_theorem(animorrl, (n((_=>n(A)))=>(n(A)=>_)), poi_000854_animorrl, 0).
poi_theorem(ianor, n(((n(n((A=>n(B))))=>(n(n(A))=>n(B)))=>n(((n(n(A))=>n(B))=>n(n((A=>n(B)))))))), poi_000855_ianor, 0).
poi_theorem(anor, n(((n((A=>n(B)))=>n((n(n(A))=>n(B))))=>n((n((n(n(A))=>n(B)))=>n((A=>n(B))))))), poi_000856_anor, 0).
poi_theorem('pm4.52', n(((n((A=>n(n(B))))=>n((n(n(A))=>B)))=>n((n((n(n(A))=>B))=>n((A=>n(n(B)))))))), 'poi_000857_pm4.52', 0).
poi_theorem('pm4.53', n(((n(n((A=>n(n(B)))))=>(n(n(A))=>B))=>n(((n(n(A))=>B)=>n(n((A=>n(n(B))))))))), 'poi_000858_pm4.53', 0).
poi_theorem('pm4.55', n(((n(n((n(A)=>n(B))))=>(n(A)=>n(B)))=>n(((n(A)=>n(B))=>n(n((n(A)=>n(B)))))))), 'poi_000859_pm4.55', 0).
poi_theorem('pm4.56', n(((n((n(A)=>n(n(B))))=>n((n(A)=>B)))=>n((n((n(A)=>B))=>n((n(A)=>n(n(B)))))))), 'poi_000860_pm4.56', 0).
poi_theorem(oran, n((((n(A)=>B)=>n(n((n(A)=>n(n(B))))))=>n((n(n((n(A)=>n(n(B)))))=>(n(A)=>B))))), poi_000861_oran, 0).
poi_theorem('pm4.57', n(((n(n((n(A)=>n(n(B)))))=>(n(A)=>B))=>n(((n(A)=>B)=>n(n((n(A)=>n(n(B))))))))), 'poi_000862_pm4.57', 0).
poi_theorem('pm3.1', (n((A=>n(B)))=>n((n(n(A))=>n(B)))), 'poi_000863_pm3.1', 0).
poi_theorem('pm3.11', (n((n(n(A))=>n(B)))=>n((A=>n(B)))), 'poi_000864_pm3.11', 0).
poi_theorem('pm3.13', (n(n((A=>n(B))))=>(n(n(A))=>n(B))), 'poi_000865_pm3.13', 0).
poi_theorem('pm3.14', ((n(n(A))=>n(B))=>n(n((A=>n(B))))), 'poi_000866_pm3.14', 0).
poi_theorem('pm4.44', n(((A=>(n(A)=>n((A=>n(B)))))=>n(((n(A)=>n((A=>n(B))))=>A)))), 'poi_000867_pm4.44', 0).
poi_theorem('pm4.45', n(((A=>n((A=>n((n(A)=>B)))))=>n((n((A=>n((n(A)=>B))))=>A)))), 'poi_000868_pm4.45', 0).
poi_theorem(orabs, n(((A=>n(((n(A)=>B)=>n(A))))=>n((n(((n(A)=>B)=>n(A)))=>A)))), poi_000869_orabs, 0).
poi_theorem(oranabs, n(((n(((n(A)=>n(B))=>n(B)))=>n((A=>n(B))))=>n((n((A=>n(B)))=>n(((n(A)=>n(B))=>n(B))))))), poi_000870_oranabs, 0.11).
poi_theorem('pm5.61', n(((n(((n(A)=>B)=>n(n(B))))=>n((A=>n(n(B)))))=>n((n((A=>n(n(B))))=>n(((n(A)=>B)=>n(n(B)))))))), 'poi_000871_pm5.61', 0.11).
poi_theorem('pm5.6', n((((n((A=>n(n(B))))=>C)=>(A=>(n(B)=>C)))=>n(((A=>(n(B)=>C))=>(n((A=>n(n(B))))=>C))))), 'poi_000872_pm5.6', 0.11).
poi_theorem(orcanai, ((A=>(n(B)=>C))=>(n((A=>n(n(B))))=>C)), poi_000873_orcanai, 0.11).
poi_theorem('pm4.79', n((((n((A=>B))=>(C=>B))=>(n((A=>n(C)))=>B))=>n(((n((A=>n(C)))=>B)=>(n((A=>B))=>(C=>B)))))), 'poi_000874_pm4.79', 0.44).
poi_theorem('pm5.53', n(((((n((n(A)=>B))=>C)=>D)=>n((n(((A=>D)=>n((B=>D))))=>n((C=>D)))))=>n((n((n(((A=>D)=>n((B=>D))))=>n((C=>D))))=>((n((n(A)=>B))=>C)=>D))))), 'poi_000875_pm5.53', 0.89).
poi_theorem(ordi, n((((n(A)=>n((B=>n(C))))=>n(((n(A)=>B)=>n((n(A)=>C)))))=>n((n(((n(A)=>B)=>n((n(A)=>C))))=>(n(A)=>n((B=>n(C)))))))), poi_000876_ordi, 0.33).
poi_theorem(ordir, n((((n(n((A=>n(B))))=>C)=>n(((n(A)=>C)=>n((n(B)=>C)))))=>n((n(((n(A)=>C)=>n((n(B)=>C))))=>(n(n((A=>n(B))))=>C))))), poi_000877_ordir, 0.33).
poi_theorem(andi, n(((n((A=>n((n(B)=>C))))=>(n(n((A=>n(B))))=>n((A=>n(C)))))=>n(((n(n((A=>n(B))))=>n((A=>n(C))))=>n((A=>n((n(B)=>C)))))))), poi_000878_andi, 0.67).
poi_theorem(andir, n(((n(((n(A)=>B)=>n(C)))=>(n(n((A=>n(C))))=>n((B=>n(C)))))=>n(((n(n((A=>n(C))))=>n((B=>n(C))))=>n(((n(A)=>B)=>n(C))))))), poi_000879_andir, 0.33).
poi_theorem(orddi, n((((n(n((A=>n(B))))=>n((C=>n(D))))=>n((n(((n(A)=>C)=>n((n(A)=>D))))=>n(n(((n(B)=>C)=>n((n(B)=>D))))))))=>n((n((n(((n(A)=>C)=>n((n(A)=>D))))=>n(n(((n(B)=>C)=>n((n(B)=>D)))))))=>(n(n((A=>n(B))))=>n((C=>n(D)))))))), poi_000880_orddi, 1).
poi_theorem(anddi, n(((n(((n(A)=>B)=>n((n(C)=>D))))=>(n((n(n((A=>n(C))))=>n((A=>n(D)))))=>(n(n((B=>n(C))))=>n((B=>n(D))))))=>n(((n((n(n((A=>n(C))))=>n((A=>n(D)))))=>(n(n((B=>n(C))))=>n((B=>n(D)))))=>n(((n(A)=>B)=>n((n(C)=>D)))))))), poi_000881_anddi, 1).
poi_theorem('pm5.17', n(((n(((n(A)=>B)=>n(n(n((A=>n(B)))))))=>n(((A=>n(B))=>n((n(B)=>A)))))=>n((n(((A=>n(B))=>n((n(B)=>A))))=>n(((n(A)=>B)=>n(n(n((A=>n(B))))))))))), 'poi_000882_pm5.17', 0.33).
poi_theorem('pm5.15', (n(n(((A=>B)=>n((B=>A)))))=>n(((A=>n(B))=>n((n(B)=>A))))), 'poi_000883_pm5.15', 0.89).
poi_theorem('pm5.16', n(n((n(((A=>B)=>n((B=>A))))=>n(n(((A=>n(B))=>n((n(B)=>A)))))))), 'poi_000884_pm5.16', 0.56).
poi_theorem(xor, n(((n(n(((A=>B)=>n((B=>A)))))=>(n(n((A=>n(n(B)))))=>n((B=>n(n(A))))))=>n(((n(n((A=>n(n(B)))))=>n((B=>n(n(A)))))=>n(n(((A=>B)=>n((B=>A))))))))), poi_000885_xor, 0.44).
poi_theorem(nbi2, n(((n(n(((A=>B)=>n((B=>A)))))=>n(((n(A)=>B)=>n(n(n((A=>n(B))))))))=>n((n(((n(A)=>B)=>n(n(n((A=>n(B)))))))=>n(n(((A=>B)=>n((B=>A))))))))), poi_000886_nbi2, 0.78).
poi_theorem(xordi, n(((n((A=>n(n(n(((B=>C)=>n((C=>B))))))))=>n(n(((n((A=>n(B)))=>n((A=>n(C))))=>n((n((A=>n(C)))=>n((A=>n(B)))))))))=>n((n(n(((n((A=>n(B)))=>n((A=>n(C))))=>n((n((A=>n(C)))=>n((A=>n(B))))))))=>n((A=>n(n(n(((B=>C)=>n((C=>B)))))))))))), poi_000887_xordi, 1).
poi_theorem('pm5.54', (n(n(((n((A=>n(B)))=>A)=>n((A=>n((A=>n(B))))))))=>n(((n((A=>n(B)))=>B)=>n((B=>n((A=>n(B)))))))), 'poi_000888_pm5.54', 0.11).
poi_theorem('pm5.62', n((((n(n((A=>n(B))))=>n(B))=>(n(A)=>n(B)))=>n(((n(A)=>n(B))=>(n(n((A=>n(B))))=>n(B)))))), 'poi_000889_pm5.62', 0).
poi_theorem('pm5.63', n((((n(A)=>B)=>(n(A)=>n((n(A)=>n(B)))))=>n(((n(A)=>n((n(A)=>n(B))))=>(n(A)=>B))))), 'poi_000890_pm5.63', 0).
poi_theorem(niabn, (A=>(n(B)=>n(((n((C=>n(B)))=>n(A))=>n((n(A)=>n((C=>n(B))))))))), poi_000891_niabn, 0.33).
poi_theorem(ninba, (A=>(n(B)=>n(((n(A)=>n((C=>n(B))))=>n((n((C=>n(B)))=>n(A))))))), poi_000892_ninba, 0.33).
poi_theorem('pm4.43', n(((A=>n(((n(A)=>B)=>n((n(A)=>n(B))))))=>n((n(((n(A)=>B)=>n((n(A)=>n(B)))))=>A)))), 'poi_000893_pm4.43', 0).
poi_theorem('pm4.82', n(((n(((A=>B)=>n((A=>n(B)))))=>n(A))=>n((n(A)=>n(((A=>B)=>n((A=>n(B))))))))), 'poi_000894_pm4.82', 0.11).
poi_theorem('pm4.83', n(((n(((A=>B)=>n((n(A)=>B))))=>B)=>n((B=>n(((A=>B)=>n((n(A)=>B)))))))), 'poi_000895_pm4.83', 0.11).
poi_theorem(pclem6, (n(((A=>n((B=>n(n(A)))))=>n((n((B=>n(n(A))))=>A))))=>n(B)), poi_000896_pclem6, 0.33).
poi_theorem(bigolden, n(((n(((n((A=>n(B)))=>A)=>n((A=>n((A=>n(B)))))))=>n(((B=>(n(A)=>B))=>n(((n(A)=>B)=>B)))))=>n((n(((B=>(n(A)=>B))=>n(((n(A)=>B)=>B))))=>n(((n((A=>n(B)))=>A)=>n((A=>n((A=>n(B))))))))))), poi_000897_bigolden, 0.78).
poi_theorem('pm5.71', ((A=>n(B))=>n(((n(((n(C)=>A)=>n(B)))=>n((C=>n(B))))=>n((n((C=>n(B)))=>n(((n(C)=>A)=>n(B)))))))), 'poi_000898_pm5.71', 0.44).
poi_theorem('pm5.75', (n(((A=>n(B))=>n(n(((C=>(n(B)=>A))=>n(((n(B)=>A)=>C)))))))=>n(((n((C=>n(n(B))))=>A)=>n((A=>n((C=>n(n(B))))))))), 'poi_000899_pm5.75', 1).
poi_theorem(ecase2d, ((A=>B)=>((A=>n(n((B=>n(C)))))=>((A=>n(n((B=>n(D)))))=>((A=>(n(E)=>(n(C)=>D)))=>(A=>E))))), poi_000900_ecase2d, 1).
poi_theorem(ecase3, ((A=>B)=>((C=>B)=>((n((n(A)=>C))=>B)=>B))), poi_000901_ecase3, 0.44).
poi_theorem(ecase, ((n(A)=>B)=>((n(C)=>B)=>((n((A=>n(C)))=>B)=>B))), poi_000902_ecase, 0.67).
poi_theorem(ecase3d, ((A=>(B=>C))=>((A=>(D=>C))=>((A=>(n((n(B)=>D))=>C))=>(A=>C)))), poi_000903_ecase3d, 1).
poi_theorem(ecased, ((A=>(n(B)=>C))=>((A=>(n(D)=>C))=>((A=>(n((B=>n(D)))=>C))=>(A=>C)))), poi_000904_ecased, 1).
poi_theorem(ecase3ad, ((A=>(B=>C))=>((A=>(D=>C))=>((A=>(n((n(B)=>n(n(D))))=>C))=>(A=>C)))), poi_000905_ecase3ad, 1).
poi_theorem(ccase, ((n((A=>n(B)))=>C)=>((n((D=>n(B)))=>C)=>((n((A=>n(E)))=>C)=>((n((D=>n(E)))=>C)=>(n(((n(A)=>D)=>n((n(B)=>E))))=>C))))), poi_000906_ccase, 1).
poi_theorem(ccased, ((A=>(n((B=>n(C)))=>D))=>((A=>(n((E=>n(C)))=>D))=>((A=>(n((B=>n(F)))=>D))=>((A=>(n((E=>n(F)))=>D))=>(A=>(n(((n(B)=>E)=>n((n(C)=>F))))=>D)))))), poi_000907_ccased, 1).
poi_theorem(ccase2, ((n((A=>n(B)))=>C)=>((D=>C)=>((E=>C)=>(n(((n(A)=>D)=>n((n(B)=>E))))=>C)))), poi_000908_ccase2, 1).
poi_theorem('4cases', ((n((A=>n(B)))=>C)=>((n((A=>n(n(B))))=>C)=>((n((n(A)=>n(B)))=>C)=>((n((n(A)=>n(n(B))))=>C)=>C)))), poi_000909_4cases, 1).
poi_theorem('4casesdan', ((n((A=>n(n((B=>n(C))))))=>D)=>((n((A=>n(n((B=>n(n(C)))))))=>D)=>((n((A=>n(n((n(B)=>n(C))))))=>D)=>((n((A=>n(n((n(B)=>n(n(C)))))))=>D)=>(A=>D))))), poi_000910_4casesdan, 1).
poi_theorem(cases, ((A=>n(((B=>C)=>n((C=>B)))))=>((n(A)=>n(((B=>D)=>n((D=>B)))))=>n(((B=>(n(n((A=>n(C))))=>n((n(A)=>n(D)))))=>n(((n(n((A=>n(C))))=>n((n(A)=>n(D))))=>B)))))), poi_000911_cases, 1).
poi_theorem(dedlem0a, (A=>n(((B=>((C=>A)=>n((B=>n(A)))))=>n((((C=>A)=>n((B=>n(A))))=>B))))), poi_000912_dedlem0a, 0.44).
poi_theorem(dedlem0b, (n(A)=>n(((B=>((B=>A)=>n((C=>n(A)))))=>n((((B=>A)=>n((C=>n(A))))=>B))))), poi_000913_dedlem0b, 0.22).
poi_theorem(dedlema, (A=>n(((B=>(n(n((B=>n(A))))=>n((C=>n(n(A))))))=>n(((n(n((B=>n(A))))=>n((C=>n(n(A)))))=>B))))), poi_000914_dedlema, 0.44).
poi_theorem(dedlemb, (n(A)=>n(((B=>(n(n((C=>n(A))))=>n((B=>n(n(A))))))=>n(((n(n((C=>n(A))))=>n((B=>n(n(A)))))=>B))))), poi_000915_dedlemb, 0.33).
poi_theorem(cases2, n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>n(((A=>B)=>n((n(A)=>C)))))=>n((n(((A=>B)=>n((n(A)=>C))))=>(n(n((A=>n(B))))=>n((n(A)=>n(C)))))))), poi_000916_cases2, 0.78).
poi_theorem(dfbi3, n(((n(((A=>B)=>n((B=>A))))=>(n(n((A=>n(B))))=>n((n(A)=>n(n(B))))))=>n(((n(n((A=>n(B))))=>n((n(A)=>n(n(B)))))=>n(((A=>B)=>n((B=>A)))))))), poi_000917_dfbi3, 0.78).
poi_theorem('pm5.24', n(((n((n(n((A=>n(B))))=>n((n(A)=>n(n(B))))))=>(n(n((A=>n(n(B)))))=>n((B=>n(n(A))))))=>n(((n(n((A=>n(n(B)))))=>n((B=>n(n(A)))))=>n((n(n((A=>n(B))))=>n((n(A)=>n(n(B)))))))))), 'poi_000918_pm5.24', 1).
poi_theorem('4exmid', (n((n(n((A=>n(B))))=>n((n(A)=>n(n(B))))))=>(n(n((A=>n(n(B)))))=>n((B=>n(n(A)))))), poi_000919_4exmid, 1).
poi_theorem(consensus, n((((n((n(n((A=>n(B))))=>n((n(A)=>n(C)))))=>n((B=>n(C))))=>(n(n((A=>n(B))))=>n((n(A)=>n(C)))))=>n(((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>(n((n(n((A=>n(B))))=>n((n(A)=>n(C)))))=>n((B=>n(C)))))))), poi_000920_consensus, 0.22).
poi_theorem('pm4.42', n(((A=>(n(n((A=>n(B))))=>n((A=>n(n(B))))))=>n(((n(n((A=>n(B))))=>n((A=>n(n(B)))))=>A)))), 'poi_000921_pm4.42', 0).
poi_theorem(prlem1, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(E))=>(A=>(D=>((n(n((D=>n(C))))=>n((E=>n(_))))=>B))))), poi_000922_prlem1, 1).
poi_theorem(prlem2, n((((n(n((A=>n(B))))=>n((C=>n(D))))=>n(((n(A)=>C)=>n((n(n((A=>n(B))))=>n((C=>n(D))))))))=>n((n(((n(A)=>C)=>n((n(n((A=>n(B))))=>n((C=>n(D)))))))=>(n(n((A=>n(B))))=>n((C=>n(D)))))))), poi_000923_prlem2, 0.11).
poi_theorem(oplem1, ((A=>(n(B)=>C))=>((A=>(n(D)=>E))=>(n(((B=>D)=>n((D=>B))))=>((C=>n(((D=>E)=>n((E=>D)))))=>(A=>B))))), poi_000924_oplem1, 1).
poi_theorem(dn1, n(((n((n(n((n(n((n(A)=>B)))=>C)))=>n((n(A)=>n((n(n(C))=>n((n(C)=>D))))))))=>C)=>n((C=>n((n(n((n(n((n(A)=>B)))=>C)))=>n((n(A)=>n((n(n(C))=>n((n(C)=>D)))))))))))), poi_000925_dn1, 0.56).
poi_theorem(bianir, (n((A=>n(n(((B=>A)=>n((A=>B)))))))=>B), poi_000926_bianir, 0.22).
poi_theorem(jaoi2, (((n(A)=>n((n(A)=>n(B))))=>C)=>((n(A)=>B)=>C)), poi_000927_jaoi2, 0).
poi_theorem(jaoi3, ((A=>B)=>((n((n(A)=>n(C)))=>B)=>((n(A)=>C)=>B))), poi_000928_jaoi3, 0.67).
poi_theorem(ornld, (A=>(n(((A=>(n(B)=>C))=>n(n(B))))=>C)), poi_000929_ornld, 0.67).
poi_theorem(dfifp4, n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>n(((n(n(A))=>B)=>n((n(A)=>C)))))=>n((n(((n(n(A))=>B)=>n((n(A)=>C))))=>(n(n((A=>n(B))))=>n((n(A)=>n(C)))))))), poi_000930_dfifp4, 1).
poi_theorem(dfifp6, n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>(n(n((A=>n(B))))=>n((C=>A))))=>n(((n(n((A=>n(B))))=>n((C=>A)))=>(n(n((A=>n(B))))=>n((n(A)=>n(C)))))))), poi_000931_dfifp6, 0.11).
poi_theorem(dfifp7, n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>((C=>A)=>n((A=>n(B)))))=>n((((C=>A)=>n((A=>n(B))))=>(n(n((A=>n(B))))=>n((n(A)=>n(C)))))))), poi_000932_dfifp7, 0.33).
poi_theorem(anifp, (n((A=>n(B)))=>(n(n((C=>n(A))))=>n((n(C)=>n(B))))), poi_000933_anifp, 0.44).
poi_theorem(ifpor, ((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>(n(B)=>C)), poi_000934_ifpor, 0.11).
poi_theorem(ifpn, n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>(n(n((n(A)=>n(C))))=>n((n(n(A))=>n(B)))))=>n(((n(n((n(A)=>n(C))))=>n((n(n(A))=>n(B))))=>(n(n((A=>n(B))))=>n((n(A)=>n(C)))))))), poi_000935_ifpn, 0).
poi_theorem(ifptru, (A=>n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>B)=>n((B=>(n(n((A=>n(B))))=>n((n(A)=>n(C))))))))), poi_000936_ifptru, 0.44).
poi_theorem(ifpfal, (n(A)=>n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>C)=>n((C=>(n(n((A=>n(B))))=>n((n(A)=>n(C))))))))), poi_000937_ifpfal, 0.44).
poi_theorem(ifpid, n((((n(n((A=>n(B))))=>n((n(A)=>n(B))))=>B)=>n((B=>(n(n((A=>n(B))))=>n((n(A)=>n(B)))))))), poi_000938_ifpid, 0.11).
poi_theorem(ifpbi123d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>((A=>n(((F=>G)=>n((G=>F)))))=>(A=>n((((n(n((B=>n(D))))=>n((n(B)=>n(F))))=>(n(n((C=>n(E))))=>n((n(C)=>n(G)))))=>n(((n(n((C=>n(E))))=>n((n(C)=>n(G))))=>(n(n((B=>n(D))))=>n((n(B)=>n(F)))))))))))), poi_000939_ifpbi123d, 1).
poi_theorem(ifpbi23d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n((((n(n((F=>n(B))))=>n((n(F)=>n(D))))=>(n(n((F=>n(C))))=>n((n(F)=>n(E)))))=>n(((n(n((F=>n(C))))=>n((n(F)=>n(E))))=>(n(n((F=>n(B))))=>n((n(F)=>n(D))))))))))), poi_000940_ifpbi23d, 1).
poi_theorem(ifpimpda, ((n((A=>n(B)))=>C)=>((n((A=>n(n(B))))=>D)=>(A=>(n(n((B=>n(C))))=>n((n(B)=>n(D))))))), poi_000941_ifpimpda, 1).
poi_theorem('1fpid3', ((n((A=>n(B)))=>C)=>((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>C)), poi_000942_1fpid3, 0.33).
poi_theorem(elimh, ((n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>B)=>n((B=>(n(n((A=>n(B))))=>n((n(A)=>n(C))))))))=>n(((D=>A)=>n((A=>D)))))=>((n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>C)=>n((C=>(n(n((A=>n(B))))=>n((n(A)=>n(C))))))))=>n(((D=>E)=>n((E=>D)))))=>(E=>D))), poi_000943_elimh, 1).
poi_theorem(dedt, ((n((((n(n((A=>n(B))))=>n((n(A)=>n(C))))=>B)=>n((B=>(n(n((A=>n(B))))=>n((n(A)=>n(C))))))))=>n(((D=>E)=>n((E=>D)))))=>(D=>(A=>E))), poi_000944_dedt, 0.89).
poi_theorem('3orel1', (n(A)=>((n((n(A)=>B))=>C)=>(n(B)=>C))), poi_000945_3orel1, 0.44).
poi_theorem('3orrot', n((((n((n(A)=>B))=>C)=>(n((n(B)=>C))=>A))=>n(((n((n(B)=>C))=>A)=>(n((n(A)=>B))=>C))))), poi_000946_3orrot, 0.67).
poi_theorem('3orcoma', n((((n((n(A)=>B))=>C)=>(n((n(B)=>A))=>C))=>n(((n((n(B)=>A))=>C)=>(n((n(A)=>B))=>C))))), poi_000947_3orcoma, 0.11).
poi_theorem('3ancoma', n(((n((n((A=>n(B)))=>n(C)))=>n((n((B=>n(A)))=>n(C))))=>n((n((n((B=>n(A)))=>n(C)))=>n((n((A=>n(B)))=>n(C))))))), poi_000948_3ancoma, 0.22).
poi_theorem('3anrot', n(((n((n((A=>n(B)))=>n(C)))=>n((n((B=>n(C)))=>n(A))))=>n((n((n((B=>n(C)))=>n(A)))=>n((n((A=>n(B)))=>n(C))))))), poi_000949_3anrot, 0.44).
poi_theorem(anandi3, n(((n((n((A=>n(B)))=>n(C)))=>n((n((A=>n(B)))=>n(n((A=>n(C)))))))=>n((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>n((n((A=>n(B)))=>n(C))))))), poi_000950_anandi3, 0).
poi_theorem(anandi3r, n(((n((n((A=>n(B)))=>n(C)))=>n((n((A=>n(B)))=>n(n((C=>n(B)))))))=>n((n((n((A=>n(B)))=>n(n((C=>n(B))))))=>n((n((A=>n(B)))=>n(C))))))), poi_000951_anandi3r, 0.11).
poi_theorem('3anidm', n(((n((n((A=>n(A)))=>n(A)))=>A)=>n((A=>n((n((A=>n(A)))=>n(A))))))), poi_000952_3anidm, 0).
poi_theorem('3an4anass', n(((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>n((n((A=>n(B)))=>n(n((C=>n(D)))))))=>n((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n((n((n((A=>n(B)))=>n(C)))=>n(D))))))), poi_000953_3an4anass, 0.78).
poi_theorem('3ioran', n(((n((n((n(A)=>B))=>C))=>n((n((n(A)=>n(n(B))))=>n(n(C)))))=>n((n((n((n(A)=>n(n(B))))=>n(n(C))))=>n((n((n(A)=>B))=>C)))))), poi_000954_3ioran, 0.67).
poi_theorem('3ianor', n(((n(n((n((A=>n(B)))=>n(C))))=>(n((n(n(A))=>n(B)))=>n(C)))=>n(((n((n(n(A))=>n(B)))=>n(C))=>n(n((n((A=>n(B)))=>n(C)))))))), poi_000955_3ianor, 0).
poi_theorem('3anor', n(((n((n((A=>n(B)))=>n(C)))=>n((n((n(n(A))=>n(B)))=>n(C))))=>n((n((n((n(n(A))=>n(B)))=>n(C)))=>n((n((A=>n(B)))=>n(C))))))), poi_000956_3anor, 0.67).
poi_theorem('3oran', n((((n((n(A)=>B))=>C)=>n(n((n((n(A)=>n(n(B))))=>n(n(C))))))=>n((n(n((n((n(A)=>n(n(B))))=>n(n(C)))))=>(n((n(A)=>B))=>C))))), poi_000957_3oran, 0.22).
poi_theorem('3imp31', ((A=>(B=>(C=>D)))=>(n((n((C=>n(B)))=>n(A)))=>D)), poi_000958_3imp31, 0.67).
poi_theorem('3imp231', ((A=>(B=>(C=>D)))=>(n((n((B=>n(C)))=>n(A)))=>D)), poi_000959_3imp231, 0.67).
poi_theorem('3imp21', ((A=>(B=>(C=>D)))=>(n((n((B=>n(A)))=>n(C)))=>D)), poi_000960_3imp21, 0.56).
poi_theorem('3impia', ((n((A=>n(B)))=>(C=>D))=>(n((n((A=>n(B)))=>n(C)))=>D)), poi_000961_3impia, 0.33).
poi_theorem('3expia', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((A=>n(B)))=>(C=>D))), poi_000962_3expia, 0.11).
poi_theorem('3comr', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((C=>n(A)))=>n(B)))=>D)), poi_000963_3comr, 0.22).
poi_theorem('3coml', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((B=>n(C)))=>n(A)))=>D)), poi_000964_3coml, 0.44).
poi_theorem('3jcad', ((A=>(B=>C))=>((A=>(B=>D))=>((A=>(B=>E))=>(A=>(B=>n((n((C=>n(D)))=>n(E)))))))), poi_000965_3jcad, 1).
poi_theorem('3adant3', ((n((A=>n(B)))=>C)=>(n((n((A=>n(B)))=>n(_)))=>C)), poi_000966_3adant3, 0).
poi_theorem('3ad2ant3', ((A=>B)=>(n((n((_=>n(_)))=>n(A)))=>B)), poi_000967_3ad2ant3, 0).
poi_theorem(simp3, (n((n((_=>n(_)))=>n(A)))=>A), poi_000968_simp3, 0).
poi_theorem(simp3d, ((A=>n((n((_=>n(_)))=>n(B))))=>(A=>B)), poi_000969_simp3d, 0).
poi_theorem(simp1bi, (n(((A=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>A))))=>(A=>B)), poi_000970_simp1bi, 0).
poi_theorem(simp2bi, (n(((A=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>A))))=>(A=>C)), poi_000971_simp2bi, 0).
poi_theorem(simp3bi, (n(((A=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>A))))=>(A=>D)), poi_000972_simp3bi, 0).
poi_theorem('3simpa', (n((n((A=>n(B)))=>n(_)))=>n((A=>n(B)))), poi_000973_3simpa, 0).
poi_theorem('3simpb', (n((n((A=>n(_)))=>n(B)))=>n((A=>n(B)))), poi_000974_3simpb, 0).
poi_theorem('3simpc', (n((n((_=>n(A)))=>n(B)))=>n((A=>n(B)))), poi_000975_3simpc, 0).
poi_theorem('3anim123i', ((A=>B)=>((C=>D)=>((E=>F)=>(n((n((A=>n(C)))=>n(E)))=>n((n((B=>n(D)))=>n(F))))))), poi_000976_3anim123i, 1).
poi_theorem('3anim1i', ((A=>B)=>(n((n((A=>n(C)))=>n(D)))=>n((n((B=>n(C)))=>n(D))))), poi_000977_3anim1i, 1).
poi_theorem('3anim2i', ((A=>B)=>(n((n((C=>n(A)))=>n(D)))=>n((n((C=>n(B)))=>n(D))))), poi_000978_3anim2i, 1).
poi_theorem('3anim3i', ((A=>B)=>(n((n((C=>n(D)))=>n(A)))=>n((n((C=>n(D)))=>n(B))))), poi_000979_3anim3i, 0.56).
poi_theorem('3anbi123i', (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>(n(((E=>F)=>n((F=>E))))=>n(((n((n((A=>n(C)))=>n(E)))=>n((n((B=>n(D)))=>n(F))))=>n((n((n((B=>n(D)))=>n(F)))=>n((n((A=>n(C)))=>n(E)))))))))), poi_000980_3anbi123i, 1).
poi_theorem('3orbi123i', (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>(n(((E=>F)=>n((F=>E))))=>n((((n((n(A)=>C))=>E)=>(n((n(B)=>D))=>F))=>n(((n((n(B)=>D))=>F)=>(n((n(A)=>C))=>E)))))))), poi_000981_3orbi123i, 1).
poi_theorem('3anbi1i', (n(((A=>B)=>n((B=>A))))=>n(((n((n((A=>n(C)))=>n(D)))=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>n((n((A=>n(C)))=>n(D)))))))), poi_000982_3anbi1i, 1).
poi_theorem('3anbi2i', (n(((A=>B)=>n((B=>A))))=>n(((n((n((C=>n(A)))=>n(D)))=>n((n((C=>n(B)))=>n(D))))=>n((n((n((C=>n(B)))=>n(D)))=>n((n((C=>n(A)))=>n(D)))))))), poi_000983_3anbi2i, 1).
poi_theorem('3anbi3i', (n(((A=>B)=>n((B=>A))))=>n(((n((n((C=>n(D)))=>n(A)))=>n((n((C=>n(D)))=>n(B))))=>n((n((n((C=>n(D)))=>n(B)))=>n((n((C=>n(D)))=>n(A)))))))), poi_000984_3anbi3i, 1).
poi_theorem(syl3an, ((A=>B)=>((C=>D)=>((E=>F)=>((n((n((B=>n(D)))=>n(F)))=>G)=>(n((n((A=>n(C)))=>n(E)))=>G))))), poi_000985_syl3an, 1).
poi_theorem(syl3anb, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>(n(((E=>F)=>n((F=>E))))=>((n((n((B=>n(D)))=>n(F)))=>G)=>(n((n((A=>n(C)))=>n(E)))=>G))))), poi_000986_syl3anb, 1).
poi_theorem(syl3anbr, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>(n(((E=>F)=>n((F=>E))))=>((n((n((A=>n(C)))=>n(E)))=>G)=>(n((n((B=>n(D)))=>n(F)))=>G))))), poi_000987_syl3anbr, 1).
poi_theorem(syl3an3, ((A=>B)=>((n((n((C=>n(D)))=>n(B)))=>E)=>(n((n((C=>n(D)))=>n(A)))=>E))), poi_000988_syl3an3, 0.78).
poi_theorem('3adantl3', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((A=>n(B)))=>n(_)))=>n(C)))=>D)), poi_000989_3adantl3, 0).
poi_theorem('3adantr3', ((n((A=>n(n((B=>n(C))))))=>D)=>(n((A=>n(n((n((B=>n(C)))=>n(_))))))=>D)), poi_000990_3adantr3, 0).
poi_theorem(ad4ant123, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((A=>n(B)))=>n(C)))=>n(_)))=>D)), poi_000991_ad4ant123, 0).
poi_theorem('3adant3l', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((A=>n(B)))=>n(n((_=>n(C))))))=>D)), poi_000992_3adant3l, 0).
poi_theorem('3adant3r', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((A=>n(B)))=>n(n((C=>n(_))))))=>D)), poi_000993_3adant3r, 0).
poi_theorem('3adant3r1', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((A=>n(n((n((_=>n(B)))=>n(C))))))=>D)), poi_000994_3adant3r1, 0.56).
poi_theorem('3adant3r2', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((A=>n(n((n((B=>n(_)))=>n(C))))))=>D)), poi_000995_3adant3r2, 0.56).
poi_theorem('3adant3r3', ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((A=>n(n((n((B=>n(C)))=>n(_))))))=>D)), poi_000996_3adant3r3, 0.67).
poi_theorem('3ad2antl3', ((n((A=>n(B)))=>C)=>(n((n((n((_=>n(_)))=>n(A)))=>n(B)))=>C)), poi_000997_3ad2antl3, 0).
poi_theorem('3ad2antr1', ((n((A=>n(B)))=>C)=>(n((A=>n(n((n((B=>n(_)))=>n(_))))))=>C)), poi_000998_3ad2antr1, 0).
poi_theorem('3ad2antr2', ((n((A=>n(B)))=>C)=>(n((A=>n(n((n((_=>n(B)))=>n(_))))))=>C)), poi_000999_3ad2antr2, 0).
poi_theorem('3ad2antr3', ((n((A=>n(B)))=>C)=>(n((A=>n(n((n((_=>n(_)))=>n(B))))))=>C)), poi_001000_3ad2antr3, 0).
poi_theorem(simpl3, (n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>A), poi_001001_simpl3, 0).
poi_theorem(simpr3, (n((_=>n(n((n((_=>n(_)))=>n(A))))))=>A), poi_001002_simpr3, 0).
poi_theorem(simp3l, (n((n((_=>n(_)))=>n(n((A=>n(_))))))=>A), poi_001003_simp3l, 0).
poi_theorem(simp3r, (n((n((_=>n(_)))=>n(n((_=>n(A))))))=>A), poi_001004_simp3r, 0).
poi_theorem(simp13, (n((n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>n(_)))=>A), poi_001005_simp13, 0).
poi_theorem(simp21, (n((n((_=>n(n((n((A=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001006_simp21, 0).
poi_theorem(simp22, (n((n((_=>n(n((n((_=>n(A)))=>n(_))))))=>n(_)))=>A), poi_001007_simp22, 0).
poi_theorem(simp23, (n((n((_=>n(n((n((_=>n(_)))=>n(A))))))=>n(_)))=>A), poi_001008_simp23, 0).
poi_theorem(simp31, (n((n((_=>n(_)))=>n(n((n((A=>n(_)))=>n(_))))))=>A), poi_001009_simp31, 0).
poi_theorem(simp32, (n((n((_=>n(_)))=>n(n((n((_=>n(A)))=>n(_))))))=>A), poi_001010_simp32, 0).
poi_theorem(simp33, (n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(A))))))=>A), poi_001011_simp33, 0).
poi_theorem(simprl1, (n((_=>n(n((n((n((A=>n(_)))=>n(_)))=>n(_))))))=>A), poi_001012_simprl1, 0).
poi_theorem(simprl2, (n((_=>n(n((n((n((_=>n(A)))=>n(_)))=>n(_))))))=>A), poi_001013_simprl2, 0).
poi_theorem(simprl3, (n((_=>n(n((n((n((_=>n(_)))=>n(A)))=>n(_))))))=>A), poi_001014_simprl3, 0).
poi_theorem(simprr1, (n((_=>n(n((_=>n(n((n((A=>n(_)))=>n(_)))))))))=>A), poi_001015_simprr1, 0).
poi_theorem(simprr2, (n((_=>n(n((_=>n(n((n((_=>n(A)))=>n(_)))))))))=>A), poi_001016_simprr2, 0).
poi_theorem(simprr3, (n((_=>n(n((_=>n(n((n((_=>n(_)))=>n(A)))))))))=>A), poi_001017_simprr3, 0).
poi_theorem(simpl2l, (n((n((n((_=>n(n((A=>n(_))))))=>n(_)))=>n(_)))=>A), poi_001018_simpl2l, 0).
poi_theorem(simpl2r, (n((n((n((_=>n(n((_=>n(A))))))=>n(_)))=>n(_)))=>A), poi_001019_simpl2r, 0).
poi_theorem(simpl3l, (n((n((n((_=>n(_)))=>n(n((A=>n(_))))))=>n(_)))=>A), poi_001020_simpl3l, 0).
poi_theorem(simpl3r, (n((n((n((_=>n(_)))=>n(n((_=>n(A))))))=>n(_)))=>A), poi_001021_simpl3r, 0).
poi_theorem(simpr2l, (n((_=>n(n((n((_=>n(n((A=>n(_))))))=>n(_))))))=>A), poi_001022_simpr2l, 0).
poi_theorem(simpr2r, (n((_=>n(n((n((_=>n(n((_=>n(A))))))=>n(_))))))=>A), poi_001023_simpr2r, 0).
poi_theorem(simpr3l, (n((_=>n(n((n((_=>n(_)))=>n(n((A=>n(_)))))))))=>A), poi_001024_simpr3l, 0).
poi_theorem(simpr3r, (n((_=>n(n((n((_=>n(_)))=>n(n((_=>n(A)))))))))=>A), poi_001025_simpr3r, 0).
poi_theorem(simp2rl, (n((n((_=>n(n((_=>n(n((A=>n(_)))))))))=>n(_)))=>A), poi_001026_simp2rl, 0).
poi_theorem(simp2rr, (n((n((_=>n(n((_=>n(n((_=>n(A)))))))))=>n(_)))=>A), poi_001027_simp2rr, 0).
poi_theorem(simp3rl, (n((n((_=>n(_)))=>n(n((_=>n(n((A=>n(_)))))))))=>A), poi_001028_simp3rl, 0).
poi_theorem(simp3rr, (n((n((_=>n(_)))=>n(n((_=>n(n((_=>n(A)))))))))=>A), poi_001029_simp3rr, 0).
poi_theorem(simpl13, (n((n((n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001030_simpl13, 0).
poi_theorem(simpl21, (n((n((n((_=>n(n((n((A=>n(_)))=>n(_))))))=>n(_)))=>n(_)))=>A), poi_001031_simpl21, 0).
poi_theorem(simpl22, (n((n((n((_=>n(n((n((_=>n(A)))=>n(_))))))=>n(_)))=>n(_)))=>A), poi_001032_simpl22, 0).
poi_theorem(simpl23, (n((n((n((_=>n(n((n((_=>n(_)))=>n(A))))))=>n(_)))=>n(_)))=>A), poi_001033_simpl23, 0).
poi_theorem(simpl31, (n((n((n((_=>n(_)))=>n(n((n((A=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001034_simpl31, 0).
poi_theorem(simpl32, (n((n((n((_=>n(_)))=>n(n((n((_=>n(A)))=>n(_))))))=>n(_)))=>A), poi_001035_simpl32, 0).
poi_theorem(simpl33, (n((n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(A))))))=>n(_)))=>A), poi_001036_simpl33, 0).
poi_theorem(simpr11, (n((_=>n(n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_))))))=>A), poi_001037_simpr11, 0).
poi_theorem(simpr12, (n((_=>n(n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_))))))=>A), poi_001038_simpr12, 0).
poi_theorem(simpr13, (n((_=>n(n((n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>n(_))))))=>A), poi_001039_simpr13, 0).
poi_theorem(simpr21, (n((_=>n(n((n((_=>n(n((n((A=>n(_)))=>n(_))))))=>n(_))))))=>A), poi_001040_simpr21, 0).
poi_theorem(simpr22, (n((_=>n(n((n((_=>n(n((n((_=>n(A)))=>n(_))))))=>n(_))))))=>A), poi_001041_simpr22, 0).
poi_theorem(simpr23, (n((_=>n(n((n((_=>n(n((n((_=>n(_)))=>n(A))))))=>n(_))))))=>A), poi_001042_simpr23, 0).
poi_theorem(simpr31, (n((_=>n(n((n((_=>n(_)))=>n(n((n((A=>n(_)))=>n(_)))))))))=>A), poi_001043_simpr31, 0).
poi_theorem(simpr32, (n((_=>n(n((n((_=>n(_)))=>n(n((n((_=>n(A)))=>n(_)))))))))=>A), poi_001044_simpr32, 0).
poi_theorem(simpr33, (n((_=>n(n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(A)))))))))=>A), poi_001045_simpr33, 0).
poi_theorem(simp2l1, (n((n((_=>n(n((n((n((A=>n(_)))=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001046_simp2l1, 0).
poi_theorem(simp2l2, (n((n((_=>n(n((n((n((_=>n(A)))=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001047_simp2l2, 0).
poi_theorem(simp2l3, (n((n((_=>n(n((n((n((_=>n(_)))=>n(A)))=>n(_))))))=>n(_)))=>A), poi_001048_simp2l3, 0).
poi_theorem(simp2r1, (n((n((_=>n(n((_=>n(n((n((A=>n(_)))=>n(_)))))))))=>n(_)))=>A), poi_001049_simp2r1, 0).
poi_theorem(simp2r2, (n((n((_=>n(n((_=>n(n((n((_=>n(A)))=>n(_)))))))))=>n(_)))=>A), poi_001050_simp2r2, 0).
poi_theorem(simp2r3, (n((n((_=>n(n((_=>n(n((n((_=>n(_)))=>n(A)))))))))=>n(_)))=>A), poi_001051_simp2r3, 0).
poi_theorem(simp3l1, (n((n((_=>n(_)))=>n(n((n((n((A=>n(_)))=>n(_)))=>n(_))))))=>A), poi_001052_simp3l1, 0).
poi_theorem(simp3l2, (n((n((_=>n(_)))=>n(n((n((n((_=>n(A)))=>n(_)))=>n(_))))))=>A), poi_001053_simp3l2, 0).
poi_theorem(simp3l3, (n((n((_=>n(_)))=>n(n((n((n((_=>n(_)))=>n(A)))=>n(_))))))=>A), poi_001054_simp3l3, 0).
poi_theorem(simp3r1, (n((n((_=>n(_)))=>n(n((_=>n(n((n((A=>n(_)))=>n(_)))))))))=>A), poi_001055_simp3r1, 0).
poi_theorem(simp3r2, (n((n((_=>n(_)))=>n(n((_=>n(n((n((_=>n(A)))=>n(_)))))))))=>A), poi_001056_simp3r2, 0).
poi_theorem(simp3r3, (n((n((_=>n(_)))=>n(n((_=>n(n((n((_=>n(_)))=>n(A)))))))))=>A), poi_001057_simp3r3, 0).
poi_theorem(simp12l, (n((n((n((n((_=>n(n((A=>n(_))))))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001058_simp12l, 0).
poi_theorem(simp12r, (n((n((n((n((_=>n(n((_=>n(A))))))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001059_simp12r, 0).
poi_theorem(simp13l, (n((n((n((n((_=>n(_)))=>n(n((A=>n(_))))))=>n(_)))=>n(_)))=>A), poi_001060_simp13l, 0).
poi_theorem(simp13r, (n((n((n((n((_=>n(_)))=>n(n((_=>n(A))))))=>n(_)))=>n(_)))=>A), poi_001061_simp13r, 0).
poi_theorem(simp22l, (n((n((_=>n(n((n((_=>n(n((A=>n(_))))))=>n(_))))))=>n(_)))=>A), poi_001062_simp22l, 0).
poi_theorem(simp22r, (n((n((_=>n(n((n((_=>n(n((_=>n(A))))))=>n(_))))))=>n(_)))=>A), poi_001063_simp22r, 0).
poi_theorem(simp23l, (n((n((_=>n(n((n((_=>n(_)))=>n(n((A=>n(_)))))))))=>n(_)))=>A), poi_001064_simp23l, 0).
poi_theorem(simp23r, (n((n((_=>n(n((n((_=>n(_)))=>n(n((_=>n(A)))))))))=>n(_)))=>A), poi_001065_simp23r, 0).
poi_theorem(simp32l, (n((n((_=>n(_)))=>n(n((n((_=>n(n((A=>n(_))))))=>n(_))))))=>A), poi_001066_simp32l, 0).
poi_theorem(simp32r, (n((n((_=>n(_)))=>n(n((n((_=>n(n((_=>n(A))))))=>n(_))))))=>A), poi_001067_simp32r, 0).
poi_theorem(simp33l, (n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(n((A=>n(_)))))))))=>A), poi_001068_simp33l, 0).
poi_theorem(simp33r, (n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(n((_=>n(A)))))))))=>A), poi_001069_simp33r, 0).
poi_theorem(simp113, (n((n((n((n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001070_simp113, 0).
poi_theorem(simp121, (n((n((n((n((_=>n(n((n((A=>n(_)))=>n(_))))))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001071_simp121, 0).
poi_theorem(simp122, (n((n((n((n((_=>n(n((n((_=>n(A)))=>n(_))))))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001072_simp122, 0).
poi_theorem(simp123, (n((n((n((n((_=>n(n((n((_=>n(_)))=>n(A))))))=>n(_)))=>n(_)))=>n(_)))=>A), poi_001073_simp123, 0).
poi_theorem(simp131, (n((n((n((n((_=>n(_)))=>n(n((n((A=>n(_)))=>n(_))))))=>n(_)))=>n(_)))=>A), poi_001074_simp131, 0).
poi_theorem(simp132, (n((n((n((n((_=>n(_)))=>n(n((n((_=>n(A)))=>n(_))))))=>n(_)))=>n(_)))=>A), poi_001075_simp132, 0).
poi_theorem(simp133, (n((n((n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(A))))))=>n(_)))=>n(_)))=>A), poi_001076_simp133, 0).
poi_theorem(simp211, (n((n((_=>n(n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001077_simp211, 0).
poi_theorem(simp212, (n((n((_=>n(n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001078_simp212, 0).
poi_theorem(simp213, (n((n((_=>n(n((n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>n(_))))))=>n(_)))=>A), poi_001079_simp213, 0).
poi_theorem(simp221, (n((n((_=>n(n((n((_=>n(n((n((A=>n(_)))=>n(_))))))=>n(_))))))=>n(_)))=>A), poi_001080_simp221, 0).
poi_theorem(simp222, (n((n((_=>n(n((n((_=>n(n((n((_=>n(A)))=>n(_))))))=>n(_))))))=>n(_)))=>A), poi_001081_simp222, 0).
poi_theorem(simp223, (n((n((_=>n(n((n((_=>n(n((n((_=>n(_)))=>n(A))))))=>n(_))))))=>n(_)))=>A), poi_001082_simp223, 0).
poi_theorem(simp231, (n((n((_=>n(n((n((_=>n(_)))=>n(n((n((A=>n(_)))=>n(_)))))))))=>n(_)))=>A), poi_001083_simp231, 0).
poi_theorem(simp232, (n((n((_=>n(n((n((_=>n(_)))=>n(n((n((_=>n(A)))=>n(_)))))))))=>n(_)))=>A), poi_001084_simp232, 0).
poi_theorem(simp233, (n((n((_=>n(n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(A)))))))))=>n(_)))=>A), poi_001085_simp233, 0).
poi_theorem(simp311, (n((n((_=>n(_)))=>n(n((n((n((n((A=>n(_)))=>n(_)))=>n(_)))=>n(_))))))=>A), poi_001086_simp311, 0).
poi_theorem(simp312, (n((n((_=>n(_)))=>n(n((n((n((n((_=>n(A)))=>n(_)))=>n(_)))=>n(_))))))=>A), poi_001087_simp312, 0).
poi_theorem(simp313, (n((n((_=>n(_)))=>n(n((n((n((n((_=>n(_)))=>n(A)))=>n(_)))=>n(_))))))=>A), poi_001088_simp313, 0).
poi_theorem(simp321, (n((n((_=>n(_)))=>n(n((n((_=>n(n((n((A=>n(_)))=>n(_))))))=>n(_))))))=>A), poi_001089_simp321, 0).
poi_theorem(simp322, (n((n((_=>n(_)))=>n(n((n((_=>n(n((n((_=>n(A)))=>n(_))))))=>n(_))))))=>A), poi_001090_simp322, 0).
poi_theorem(simp323, (n((n((_=>n(_)))=>n(n((n((_=>n(n((n((_=>n(_)))=>n(A))))))=>n(_))))))=>A), poi_001091_simp323, 0).
poi_theorem(simp331, (n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(n((n((A=>n(_)))=>n(_)))))))))=>A), poi_001092_simp331, 0).
poi_theorem(simp332, (n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(n((n((_=>n(A)))=>n(_)))))))))=>A), poi_001093_simp332, 0).
poi_theorem(simp333, (n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(n((n((_=>n(_)))=>n(A)))))))))=>A), poi_001094_simp333, 0).
poi_theorem('3anibar', ((n((n((A=>n(B)))=>n(C)))=>n(((D=>n((C=>n(E))))=>n((n((C=>n(E)))=>D)))))=>(n((n((A=>n(B)))=>n(C)))=>n(((D=>E)=>n((E=>D)))))), poi_001095_3anibar, 1).
poi_theorem('3mix1', (A=>(n((n(A)=>_))=>_)), poi_001096_3mix1, 0).
poi_theorem('3mix2', (A=>(n((n(_)=>A))=>_)), poi_001097_3mix2, 0).
poi_theorem('3mix3', (A=>(n((n(_)=>_))=>A)), poi_001098_3mix3, 0).
poi_theorem('3mix1d', ((A=>B)=>(A=>(n((n(B)=>_))=>_))), poi_001099_3mix1d, 0).
poi_theorem('3mix2d', ((A=>B)=>(A=>(n((n(_)=>B))=>_))), poi_001100_3mix2d, 0).
poi_theorem('3mix3d', ((A=>B)=>(A=>(n((n(_)=>_))=>B))), poi_001101_3mix3d, 0).
poi_theorem('pm3.2an3', (A=>(B=>(C=>n((n((A=>n(B)))=>n(C)))))), 'poi_001102_pm3.2an3', 0.78).
poi_theorem(mpbir3an, (A=>(B=>(C=>(n(((D=>n((n((A=>n(B)))=>n(C))))=>n((n((n((A=>n(B)))=>n(C)))=>D))))=>D)))), poi_001103_mpbir3an, 1).
poi_theorem(mpbir3and, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>n(((E=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>E)))))=>(A=>E))))), poi_001104_mpbir3and, 1).
poi_theorem(syl3anbrc, ((A=>B)=>((A=>C)=>((A=>D)=>(n(((E=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>E))))=>(A=>E))))), poi_001105_syl3anbrc, 1).
poi_theorem('3imp3i2an', ((n((n((A=>n(B)))=>n(C)))=>D)=>((n((A=>n(C)))=>E)=>((n((D=>n(E)))=>F)=>(n((n((A=>n(B)))=>n(C)))=>F)))), poi_001106_3imp3i2an, 1).
poi_theorem(ex3, ((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)=>(n((n((A=>n(B)))=>n(C)))=>(D=>E))), poi_001107_ex3, 0.67).
poi_theorem('3impdi', ((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>D)=>(n((n((A=>n(B)))=>n(C)))=>D)), poi_001108_3impdi, 0.11).
poi_theorem(exp5o, ((n((n((A=>n(B)))=>n(C)))=>(n((D=>n(E)))=>F))=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_001109_exp5o, 1).
poi_theorem(exp516, ((n((n((A=>n(n((n((B=>n(C)))=>n(D))))))=>n(E)))=>F)=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_001110_exp516, 1).
poi_theorem(exp520, ((n((n((n((A=>n(B)))=>n(C)))=>n(n((D=>n(E))))))=>F)=>(A=>(B=>(C=>(D=>(E=>F)))))), poi_001111_exp520, 1).
poi_theorem('3impexp', n((((n((n((A=>n(B)))=>n(C)))=>D)=>(A=>(B=>(C=>D))))=>n(((A=>(B=>(C=>D)))=>(n((n((A=>n(B)))=>n(C)))=>D))))), poi_001112_3impexp, 0.78).
poi_theorem('3an1rs', ((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)=>(n((n((n((A=>n(B)))=>n(D)))=>n(C)))=>E)), poi_001113_3an1rs, 0.22).
poi_theorem('3anassrs', ((n((A=>n(n((n((B=>n(C)))=>n(D))))))=>E)=>(n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)), poi_001114_3anassrs, 0.89).
poi_theorem(ad5ant245, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((_=>n(A)))=>n(_)))=>n(B)))=>n(C)))=>D)), poi_001115_ad5ant245, 0.11).
poi_theorem(ad5ant234, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((_=>n(A)))=>n(B)))=>n(C)))=>n(_)))=>D)), poi_001116_ad5ant234, 0).
poi_theorem(ad5ant235, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((_=>n(A)))=>n(B)))=>n(_)))=>n(C)))=>D)), poi_001117_ad5ant235, 0).
poi_theorem(ad5ant123, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((A=>n(B)))=>n(C)))=>n(_)))=>n(_)))=>D)), poi_001118_ad5ant123, 0).
poi_theorem(ad5ant124, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((A=>n(B)))=>n(_)))=>n(C)))=>n(_)))=>D)), poi_001119_ad5ant124, 0).
poi_theorem(ad5ant125, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((A=>n(B)))=>n(_)))=>n(_)))=>n(C)))=>D)), poi_001120_ad5ant125, 0).
poi_theorem(ad5ant134, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((A=>n(_)))=>n(B)))=>n(C)))=>n(_)))=>D)), poi_001121_ad5ant134, 0.11).
poi_theorem(ad5ant135, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((A=>n(_)))=>n(B)))=>n(_)))=>n(C)))=>D)), poi_001122_ad5ant135, 0.11).
poi_theorem(ad5ant145, ((n((n((A=>n(B)))=>n(C)))=>D)=>(n((n((n((n((A=>n(_)))=>n(_)))=>n(B)))=>n(C)))=>D)), poi_001123_ad5ant145, 0).
poi_theorem(ad5ant2345, ((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)=>(n((n((n((n((_=>n(A)))=>n(B)))=>n(C)))=>n(D)))=>E)), poi_001124_ad5ant2345, 0.11).
poi_theorem(syl13anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((n((B=>n(n((n((C=>n(D)))=>n(E))))))=>F)=>(A=>F)))))), poi_001125_syl13anc, 1).
poi_theorem(syl121anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((n((n((B=>n(n((C=>n(D))))))=>n(E)))=>F)=>(A=>F)))))), poi_001126_syl121anc, 1).
poi_theorem(syl23anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((n((n((B=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>G)=>(A=>G))))))), poi_001127_syl23anc, 1).
poi_theorem(syl32anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((n((n((n((B=>n(C)))=>n(D)))=>n(n((E=>n(F))))))=>G)=>(A=>G))))))), poi_001128_syl32anc, 1).
poi_theorem(syl122anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((n((n((B=>n(n((C=>n(D))))))=>n(n((E=>n(F))))))=>G)=>(A=>G))))))), poi_001129_syl122anc, 1).
poi_theorem(syl221anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((n((n((n((B=>n(C)))=>n(n((D=>n(E))))))=>n(F)))=>G)=>(A=>G))))))), poi_001130_syl221anc, 1).
poi_theorem(syl131anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((n((n((B=>n(n((n((C=>n(D)))=>n(E))))))=>n(F)))=>G)=>(A=>G))))))), poi_001131_syl131anc, 1).
poi_theorem(syl311anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(E)))=>n(F)))=>G)=>(A=>G))))))), poi_001132_syl311anc, 1).
poi_theorem(syl33anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((n((B=>n(C)))=>n(D)))=>n(n((n((E=>n(F)))=>n(G))))))=>H)=>(A=>H)))))))), poi_001133_syl33anc, 1).
poi_theorem(syl222anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((n((B=>n(C)))=>n(n((D=>n(E))))))=>n(n((F=>n(G))))))=>H)=>(A=>H)))))))), poi_001134_syl222anc, 1).
poi_theorem(syl123anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((B=>n(n((C=>n(D))))))=>n(n((n((E=>n(F)))=>n(G))))))=>H)=>(A=>H)))))))), poi_001135_syl123anc, 1).
poi_theorem(syl132anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((B=>n(n((n((C=>n(D)))=>n(E))))))=>n(n((F=>n(G))))))=>H)=>(A=>H)))))))), poi_001136_syl132anc, 1).
poi_theorem(syl231anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((n((B=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>n(G)))=>H)=>(A=>H)))))))), poi_001137_syl231anc, 1).
poi_theorem(syl312anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(E)))=>n(n((F=>n(G))))))=>H)=>(A=>H)))))))), poi_001138_syl312anc, 1).
poi_theorem(syl321anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(n((E=>n(F))))))=>n(G)))=>H)=>(A=>H)))))))), poi_001139_syl321anc, 1).
poi_theorem(syl133anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((n((n((B=>n(n((n((C=>n(D)))=>n(E))))))=>n(n((n((F=>n(G)))=>n(H))))))=>I)=>(A=>I))))))))), poi_001140_syl133anc, 1).
poi_theorem(syl313anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(E)))=>n(n((n((F=>n(G)))=>n(H))))))=>I)=>(A=>I))))))))), poi_001141_syl313anc, 1).
poi_theorem(syl331anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(n((n((E=>n(F)))=>n(G))))))=>n(H)))=>I)=>(A=>I))))))))), poi_001142_syl331anc, 1).
poi_theorem(syl223anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((n((n((n((B=>n(C)))=>n(n((D=>n(E))))))=>n(n((n((F=>n(G)))=>n(H))))))=>I)=>(A=>I))))))))), poi_001143_syl223anc, 1).
poi_theorem(syl232anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((n((n((n((B=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>n(n((G=>n(H))))))=>I)=>(A=>I))))))))), poi_001144_syl232anc, 1).
poi_theorem(syl322anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(n((E=>n(F))))))=>n(n((G=>n(H))))))=>I)=>(A=>I))))))))), poi_001145_syl322anc, 1).
poi_theorem(syl233anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((A=>I)=>((n((n((n((B=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>n(n((n((G=>n(H)))=>n(I))))))=>J)=>(A=>J)))))))))), poi_001146_syl233anc, 1).
poi_theorem(syl323anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((A=>I)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(n((E=>n(F))))))=>n(n((n((G=>n(H)))=>n(I))))))=>J)=>(A=>J)))))))))), poi_001147_syl323anc, 1).
poi_theorem(syl332anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((A=>I)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(n((n((E=>n(F)))=>n(G))))))=>n(n((H=>n(I))))))=>J)=>(A=>J)))))))))), poi_001148_syl332anc, 1).
poi_theorem(syl333anc, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>E)=>((A=>F)=>((A=>G)=>((A=>H)=>((A=>I)=>((A=>J)=>((n((n((n((n((B=>n(C)))=>n(D)))=>n(n((n((E=>n(F)))=>n(G))))))=>n(n((n((H=>n(I)))=>n(J))))))=>K)=>(A=>K))))))))))), poi_001149_syl333anc, 1).
poi_theorem(syl3an1b, (n(((A=>B)=>n((B=>A))))=>((n((n((B=>n(C)))=>n(D)))=>E)=>(n((n((A=>n(C)))=>n(D)))=>E))), poi_001150_syl3an1b, 1).
poi_theorem(syl3an2b, (n(((A=>B)=>n((B=>A))))=>((n((n((C=>n(B)))=>n(D)))=>E)=>(n((n((C=>n(A)))=>n(D)))=>E))), poi_001151_syl3an2b, 1).
poi_theorem(syl3an3b, (n(((A=>B)=>n((B=>A))))=>((n((n((C=>n(D)))=>n(B)))=>E)=>(n((n((C=>n(D)))=>n(A)))=>E))), poi_001152_syl3an3b, 1).
poi_theorem(syl3an1br, (n(((A=>B)=>n((B=>A))))=>((n((n((A=>n(C)))=>n(D)))=>E)=>(n((n((B=>n(C)))=>n(D)))=>E))), poi_001153_syl3an1br, 1).
poi_theorem(syl3an2br, (n(((A=>B)=>n((B=>A))))=>((n((n((C=>n(A)))=>n(D)))=>E)=>(n((n((C=>n(B)))=>n(D)))=>E))), poi_001154_syl3an2br, 0.78).
poi_theorem(syl3an3br, (n(((A=>B)=>n((B=>A))))=>((n((n((C=>n(D)))=>n(A)))=>E)=>(n((n((C=>n(D)))=>n(B)))=>E))), poi_001155_syl3an3br, 1).
poi_theorem(syld3an3, ((n((n((A=>n(B)))=>n(C)))=>D)=>((n((n((A=>n(B)))=>n(D)))=>E)=>(n((n((A=>n(B)))=>n(C)))=>E))), poi_001156_syld3an3, 0.78).
poi_theorem(syld3an1, ((n((n((A=>n(B)))=>n(C)))=>D)=>((n((n((D=>n(B)))=>n(C)))=>E)=>(n((n((A=>n(B)))=>n(C)))=>E))), poi_001157_syld3an1, 1).
poi_theorem(syld3an2, ((n((n((A=>n(B)))=>n(C)))=>D)=>((n((n((A=>n(D)))=>n(C)))=>E)=>(n((n((A=>n(B)))=>n(C)))=>E))), poi_001158_syld3an2, 1).
poi_theorem(syl3anl1, ((A=>B)=>((n((n((n((B=>n(C)))=>n(D)))=>n(E)))=>F)=>(n((n((n((A=>n(C)))=>n(D)))=>n(E)))=>F))), poi_001159_syl3anl1, 1).
poi_theorem(syl3anl2, ((A=>B)=>((n((n((n((C=>n(B)))=>n(D)))=>n(E)))=>F)=>(n((n((n((C=>n(A)))=>n(D)))=>n(E)))=>F))), poi_001160_syl3anl2, 1).
poi_theorem(syl3anl3, ((A=>B)=>((n((n((n((C=>n(D)))=>n(B)))=>n(E)))=>F)=>(n((n((n((C=>n(D)))=>n(A)))=>n(E)))=>F))), poi_001161_syl3anl3, 1).
poi_theorem(syl3anl, ((A=>B)=>((C=>D)=>((E=>F)=>((n((n((n((B=>n(D)))=>n(F)))=>n(G)))=>H)=>(n((n((n((A=>n(C)))=>n(E)))=>n(G)))=>H))))), poi_001162_syl3anl, 1).
poi_theorem(syl3anr1, ((A=>B)=>((n((C=>n(n((n((B=>n(D)))=>n(E))))))=>F)=>(n((C=>n(n((n((A=>n(D)))=>n(E))))))=>F))), poi_001163_syl3anr1, 1).
poi_theorem(syl3anr2, ((A=>B)=>((n((C=>n(n((n((D=>n(B)))=>n(E))))))=>F)=>(n((C=>n(n((n((D=>n(A)))=>n(E))))))=>F))), poi_001164_syl3anr2, 1).
poi_theorem(syl3anr3, ((A=>B)=>((n((C=>n(n((n((D=>n(E)))=>n(B))))))=>F)=>(n((C=>n(n((n((D=>n(E)))=>n(A))))))=>F))), poi_001165_syl3anr3, 1).
poi_theorem(syl2an3an, ((A=>B)=>((A=>C)=>((D=>E)=>((n((n((B=>n(C)))=>n(E)))=>F)=>(n((A=>n(D)))=>F))))), poi_001166_syl2an3an, 1).
poi_theorem(syl2an23an, ((A=>B)=>((A=>C)=>((n((D=>n(A)))=>E)=>((n((n((B=>n(C)))=>n(E)))=>F)=>(n((D=>n(A)))=>F))))), poi_001167_syl2an23an, 1).
poi_theorem('3ori', ((n((n(A)=>B))=>C)=>(n((n(A)=>n(n(B))))=>C)), poi_001168_3ori, 0).
poi_theorem('3jao', (n((n(((A=>B)=>n((C=>B))))=>n((D=>B))))=>((n((n(A)=>C))=>D)=>B)), poi_001169_3jao, 1).
poi_theorem('3jaoi', ((A=>B)=>((C=>B)=>((D=>B)=>((n((n(A)=>C))=>D)=>B)))), poi_001170_3jaoi, 0.78).
poi_theorem('3jaod', ((A=>(B=>C))=>((A=>(D=>C))=>((A=>(E=>C))=>(A=>((n((n(B)=>D))=>E)=>C))))), poi_001171_3jaod, 1).
poi_theorem('3jaoian', ((n((A=>n(B)))=>C)=>((n((D=>n(B)))=>C)=>((n((E=>n(B)))=>C)=>(n(((n((n(A)=>D))=>E)=>n(B)))=>C)))), poi_001172_3jaoian, 1).
poi_theorem('3jaodan', ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>C)=>((n((A=>n(E)))=>C)=>(n((A=>n((n((n(B)=>D))=>E))))=>C)))), poi_001173_3jaodan, 1).
poi_theorem(mpjao3dan, ((n((A=>n(B)))=>C)=>((n((A=>n(D)))=>C)=>((n((A=>n(E)))=>C)=>((A=>(n((n(B)=>D))=>E))=>(A=>C))))), poi_001174_mpjao3dan, 1).
poi_theorem('3jaao', ((A=>(B=>C))=>((D=>(E=>C))=>((F=>(G=>C))=>(n((n((A=>n(D)))=>n(F)))=>((n((n(B)=>E))=>G)=>C))))), poi_001175_3jaao, 1).
poi_theorem(syl3an9b, ((A=>n(((B=>C)=>n((C=>B)))))=>((D=>n(((C=>E)=>n((E=>C)))))=>((F=>n(((E=>G)=>n((G=>E)))))=>(n((n((A=>n(D)))=>n(F)))=>n(((B=>G)=>n((G=>B)))))))), poi_001176_syl3an9b, 1).
poi_theorem('3orbi123d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>((A=>n(((F=>G)=>n((G=>F)))))=>(A=>n((((n((n(B)=>D))=>F)=>(n((n(C)=>E))=>G))=>n(((n((n(C)=>E))=>G)=>(n((n(B)=>D))=>F))))))))), poi_001177_3orbi123d, 1).
poi_theorem('3anbi123d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>((A=>n(((F=>G)=>n((G=>F)))))=>(A=>n(((n((n((B=>n(D)))=>n(F)))=>n((n((C=>n(E)))=>n(G))))=>n((n((n((C=>n(E)))=>n(G)))=>n((n((B=>n(D)))=>n(F))))))))))), poi_001178_3anbi123d, 1).
poi_theorem('3anbi12d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n((n((B=>n(D)))=>n(F)))=>n((n((C=>n(E)))=>n(F))))=>n((n((n((C=>n(E)))=>n(F)))=>n((n((B=>n(D)))=>n(F)))))))))), poi_001179_3anbi12d, 1).
poi_theorem('3anbi13d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n((n((B=>n(F)))=>n(D)))=>n((n((C=>n(F)))=>n(E))))=>n((n((n((C=>n(F)))=>n(E)))=>n((n((B=>n(F)))=>n(D)))))))))), poi_001180_3anbi13d, 1).
poi_theorem('3anbi23d', ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n((n((F=>n(B)))=>n(D)))=>n((n((F=>n(C)))=>n(E))))=>n((n((n((F=>n(C)))=>n(E)))=>n((n((F=>n(B)))=>n(D)))))))))), poi_001181_3anbi23d, 1).
poi_theorem('3anbi1d', ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n((n((B=>n(D)))=>n(E)))=>n((n((C=>n(D)))=>n(E))))=>n((n((n((C=>n(D)))=>n(E)))=>n((n((B=>n(D)))=>n(E))))))))), poi_001182_3anbi1d, 1).
poi_theorem('3anbi2d', ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n((n((D=>n(B)))=>n(E)))=>n((n((D=>n(C)))=>n(E))))=>n((n((n((D=>n(C)))=>n(E)))=>n((n((D=>n(B)))=>n(E))))))))), poi_001183_3anbi2d, 1).
poi_theorem('3anbi3d', ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n((n((D=>n(E)))=>n(B)))=>n((n((D=>n(E)))=>n(C))))=>n((n((n((D=>n(E)))=>n(C)))=>n((n((D=>n(E)))=>n(B))))))))), poi_001184_3anbi3d, 1).
poi_theorem('3anim123d', ((A=>(B=>C))=>((A=>(D=>E))=>((A=>(F=>G))=>(A=>(n((n((B=>n(D)))=>n(F)))=>n((n((C=>n(E)))=>n(G)))))))), poi_001185_3anim123d, 1).
poi_theorem('3orim123d', ((A=>(B=>C))=>((A=>(D=>E))=>((A=>(F=>G))=>(A=>((n((n(B)=>D))=>F)=>(n((n(C)=>E))=>G)))))), poi_001186_3orim123d, 1).
poi_theorem(an6, n(((n((n((n((A=>n(B)))=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>n((n((n((A=>n(D)))=>n(n((B=>n(E))))))=>n(n((C=>n(F)))))))=>n((n((n((n((A=>n(D)))=>n(n((B=>n(E))))))=>n(n((C=>n(F))))))=>n((n((n((A=>n(B)))=>n(C)))=>n(n((n((D=>n(E)))=>n(F)))))))))), poi_001187_an6, 1).
poi_theorem('3an6', n(((n((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n(n((E=>n(F))))))=>n((n((n((A=>n(C)))=>n(E)))=>n(n((n((B=>n(D)))=>n(F)))))))=>n((n((n((n((A=>n(C)))=>n(E)))=>n(n((n((B=>n(D)))=>n(F))))))=>n((n((n((A=>n(B)))=>n(n((C=>n(D))))))=>n(n((E=>n(F)))))))))), poi_001188_3an6, 1).
poi_theorem('3or6', n((((n((n((n(A)=>B))=>(n(C)=>D)))=>(n(E)=>F))=>(n((n((n(A)=>C))=>E))=>(n((n(B)=>D))=>F)))=>n(((n((n((n(A)=>C))=>E))=>(n((n(B)=>D))=>F))=>(n((n((n(A)=>B))=>(n(C)=>D)))=>(n(E)=>F)))))), poi_001189_3or6, 1).
poi_theorem(mp3an3, (A=>((n((n((B=>n(C)))=>n(A)))=>D)=>(n((B=>n(C)))=>D))), poi_001190_mp3an3, 0.67).
poi_theorem(mp3an13, (A=>(B=>((n((n((A=>n(C)))=>n(B)))=>D)=>(C=>D)))), poi_001191_mp3an13, 0.78).
poi_theorem(mp3an23, (A=>(B=>((n((n((C=>n(A)))=>n(B)))=>D)=>(C=>D)))), poi_001192_mp3an23, 1).
poi_theorem(mp3an1i, (A=>((B=>(n((n((A=>n(C)))=>n(D)))=>E))=>(B=>(n((C=>n(D)))=>E)))), poi_001193_mp3an1i, 1).
poi_theorem(mp3anl1, (A=>((n((n((n((A=>n(B)))=>n(C)))=>n(D)))=>E)=>(n((n((B=>n(C)))=>n(D)))=>E))), poi_001194_mp3anl1, 1).
poi_theorem(mp3anl2, (A=>((n((n((n((B=>n(A)))=>n(C)))=>n(D)))=>E)=>(n((n((B=>n(C)))=>n(D)))=>E))), poi_001195_mp3anl2, 1).
poi_theorem(mp3anl3, (A=>((n((n((n((B=>n(C)))=>n(A)))=>n(D)))=>E)=>(n((n((B=>n(C)))=>n(D)))=>E))), poi_001196_mp3anl3, 1).
poi_theorem(mp3anr1, (A=>((n((B=>n(n((n((A=>n(C)))=>n(D))))))=>E)=>(n((B=>n(n((C=>n(D))))))=>E))), poi_001197_mp3anr1, 1).
poi_theorem(mp3anr2, (A=>((n((B=>n(n((n((C=>n(A)))=>n(D))))))=>E)=>(n((B=>n(n((C=>n(D))))))=>E))), poi_001198_mp3anr2, 1).
poi_theorem(mp3anr3, (A=>((n((B=>n(n((n((C=>n(D)))=>n(A))))))=>E)=>(n((B=>n(n((C=>n(D))))))=>E))), poi_001199_mp3anr3, 1).
poi_theorem(mp3an, (A=>(B=>(C=>((n((n((A=>n(B)))=>n(C)))=>D)=>D)))), poi_001200_mp3an, 0.78).
poi_theorem(mpd3an3, ((n((A=>n(B)))=>C)=>((n((n((A=>n(B)))=>n(C)))=>D)=>(n((A=>n(B)))=>D))), poi_001201_mpd3an3, 0.78).
poi_theorem(mpd3an23, ((A=>B)=>((A=>C)=>((n((n((A=>n(B)))=>n(C)))=>D)=>(A=>D)))), poi_001202_mpd3an23, 1).
poi_theorem(mp3and, ((A=>B)=>((A=>C)=>((A=>D)=>((A=>(n((n((B=>n(C)))=>n(D)))=>E))=>(A=>E))))), poi_001203_mp3and, 1).
poi_theorem(mp3an12i, (A=>(B=>((C=>D)=>((n((n((A=>n(B)))=>n(D)))=>E)=>(C=>E))))), poi_001204_mp3an12i, 1).
poi_theorem(mp3an2i, (A=>((B=>C)=>((B=>D)=>((n((n((A=>n(C)))=>n(D)))=>E)=>(B=>E))))), poi_001205_mp3an2i, 1).
poi_theorem(mp3an3an, (A=>((B=>C)=>((D=>E)=>((n((n((A=>n(C)))=>n(E)))=>F)=>(n((B=>n(D)))=>F))))), poi_001206_mp3an3an, 1).
poi_theorem(mp3an2ani, (A=>((B=>C)=>((n((B=>n(D)))=>E)=>((n((n((A=>n(C)))=>n(E)))=>F)=>(n((B=>n(D)))=>F))))), poi_001207_mp3an2ani, 1).
poi_theorem(biimp3a, ((n((A=>n(B)))=>n(((C=>D)=>n((D=>C)))))=>(n((n((A=>n(B)))=>n(C)))=>D)), poi_001208_biimp3a, 0.44).
poi_theorem(biimp3ar, ((n((A=>n(B)))=>n(((C=>D)=>n((D=>C)))))=>(n((n((A=>n(B)))=>n(D)))=>C)), poi_001209_biimp3ar, 0.33).
poi_theorem('3anandis', ((n((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>n(n((A=>n(D))))))=>E)=>(n((A=>n(n((n((B=>n(C)))=>n(D))))))=>E)), poi_001210_3anandis, 1).
poi_theorem('3anandirs', ((n((n((n((A=>n(B)))=>n(n((C=>n(B))))))=>n(n((D=>n(B))))))=>E)=>(n((n((n((A=>n(C)))=>n(D)))=>n(B)))=>E)), poi_001211_3anandirs, 1).
poi_theorem(ecase23d, ((A=>n(B))=>((A=>n(C))=>((A=>(n((n(D)=>B))=>C))=>(A=>D)))), poi_001212_ecase23d, 1).
poi_theorem('3ecase', ((n(A)=>B)=>((n(C)=>B)=>((n(D)=>B)=>((n((n((A=>n(C)))=>n(D)))=>B)=>B)))), poi_001213_3ecase, 1).
poi_theorem('3bior1fd', ((A=>n(B))=>(A=>n((((n(C)=>D)=>(n((n(B)=>C))=>D))=>n(((n((n(B)=>C))=>D)=>(n(C)=>D))))))), poi_001214_3bior1fd, 0.33).
poi_theorem('3bior1fand', ((A=>n(B))=>(A=>n((((n(C)=>D)=>(n((n(n((B=>n(E))))=>C))=>D))=>n(((n((n(n((B=>n(E))))=>C))=>D)=>(n(C)=>D))))))), poi_001215_3bior1fand, 0.44).
poi_theorem('3bior2fd', ((A=>n(B))=>((A=>n(C))=>(A=>n(((D=>(n((n(B)=>C))=>D))=>n(((n((n(B)=>C))=>D)=>D))))))), poi_001216_3bior2fd, 1).
poi_theorem('3biant1d', ((A=>B)=>(A=>n(((n((C=>n(D)))=>n((n((B=>n(C)))=>n(D))))=>n((n((n((B=>n(C)))=>n(D)))=>n((C=>n(D))))))))), poi_001217_3biant1d, 0.89).
poi_theorem(intn3an1d, ((A=>n(B))=>(A=>n(n((n((B=>n(_)))=>n(_)))))), poi_001218_intn3an1d, 0).
poi_theorem(intn3an2d, ((A=>n(B))=>(A=>n(n((n((_=>n(B)))=>n(_)))))), poi_001219_intn3an2d, 0).
poi_theorem(intn3an3d, ((A=>n(B))=>(A=>n(n((n((_=>n(_)))=>n(B)))))), poi_001220_intn3an3d, 0).
poi_theorem(an3andi, n(((n((A=>n(n((n((B=>n(C)))=>n(D))))))=>n((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>n(n((A=>n(D)))))))=>n((n((n((n((A=>n(B)))=>n(n((A=>n(C))))))=>n(n((A=>n(D))))))=>n((A=>n(n((n((B=>n(C)))=>n(D)))))))))), poi_001221_an3andi, 0.89).
poi_theorem(an33rean, n(((n((n((n((n((A=>n(B)))=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>n(n((n((G=>n(H)))=>n(I))))))=>n((n((n((A=>n(E)))=>n(I)))=>n(n((n((n((B=>n(D)))=>n(n((F=>n(H))))))=>n(n((C=>n(G))))))))))=>n((n((n((n((A=>n(E)))=>n(I)))=>n(n((n((n((B=>n(D)))=>n(n((F=>n(H))))))=>n(n((C=>n(G)))))))))=>n((n((n((n((A=>n(B)))=>n(C)))=>n(n((n((D=>n(E)))=>n(F))))))=>n(n((n((G=>n(H)))=>n(I)))))))))), poi_001222_an33rean, 1).
poi_theorem('3orel2', (n(A)=>((n((n(B)=>A))=>C)=>(n(B)=>C))), poi_001223_3orel2, 0.67).
poi_theorem('3orel3', (n(A)=>((n((n(B)=>C))=>A)=>(n(B)=>C))), poi_001224_3orel3, 0.11).
poi_theorem('3orel13', (n((n(A)=>n(n(B))))=>((n((n(A)=>C))=>B)=>C)), poi_001225_3orel13, 0.56).
poi_theorem('3pm3.2ni', (n(A)=>(n(B)=>(n(C)=>n((n((n(A)=>B))=>C))))), 'poi_001226_3pm3.2ni', 0.78).
poi_theorem(dfnan2, n(((n(n((A=>n(B))))=>(A=>n(B)))=>n(((A=>n(B))=>n(n((A=>n(B)))))))), poi_001227_dfnan2, 0).
poi_theorem(nancom, n(((n(n((A=>n(B))))=>n(n((B=>n(A)))))=>n((n(n((B=>n(A))))=>n(n((A=>n(B)))))))), poi_001228_nancom, 0).
poi_theorem(nannan, n(((n(n((A=>n(n(n((B=>n(C))))))))=>(A=>n((B=>n(C)))))=>n(((A=>n((B=>n(C))))=>n(n((A=>n(n(n((B=>n(C)))))))))))), poi_001229_nannan, 0).
poi_theorem(nanim, n((((A=>B)=>n(n((A=>n(n(n((B=>n(B)))))))))=>n((n(n((A=>n(n(n((B=>n(B))))))))=>(A=>B))))), poi_001230_nanim, 0).
poi_theorem(nannot, n(((n(A)=>n(n((A=>n(A)))))=>n((n(n((A=>n(A))))=>n(A))))), poi_001231_nannot, 0).
poi_theorem(nanbi, n(((n(((A=>B)=>n((B=>A))))=>n(n((n(n((A=>n(B))))=>n(n(n((n(n((A=>n(A))))=>n(n(n((B=>n(B)))))))))))))=>n((n(n((n(n((A=>n(B))))=>n(n(n((n(n((A=>n(A))))=>n(n(n((B=>n(B))))))))))))=>n(((A=>B)=>n((B=>A)))))))), poi_001232_nanbi, 1).
poi_theorem(nanbi1, (n(((A=>B)=>n((B=>A))))=>n(((n(n((A=>n(C))))=>n(n((B=>n(C)))))=>n((n(n((B=>n(C))))=>n(n((A=>n(C))))))))), poi_001233_nanbi1, 1).
poi_theorem(nanbi2, (n(((A=>B)=>n((B=>A))))=>n(((n(n((C=>n(A))))=>n(n((C=>n(B)))))=>n((n(n((C=>n(B))))=>n(n((C=>n(A))))))))), poi_001234_nanbi2, 1).
poi_theorem(nanbi12, (n((n(((A=>B)=>n((B=>A))))=>n(n(((C=>D)=>n((D=>C)))))))=>n(((n(n((A=>n(C))))=>n(n((B=>n(D)))))=>n((n(n((B=>n(D))))=>n(n((A=>n(C))))))))), poi_001235_nanbi12, 1).
poi_theorem(nanbi12i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n(((n(n((A=>n(C))))=>n(n((B=>n(D)))))=>n((n(n((B=>n(D))))=>n(n((A=>n(C)))))))))), poi_001236_nanbi12i, 1).
poi_theorem(nanbi1d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n(n((B=>n(D))))=>n(n((C=>n(D)))))=>n((n(n((C=>n(D))))=>n(n((B=>n(D)))))))))), poi_001237_nanbi1d, 1).
poi_theorem(nanbi2d, ((A=>n(((B=>C)=>n((C=>B)))))=>(A=>n(((n(n((D=>n(B))))=>n(n((D=>n(C)))))=>n((n(n((D=>n(C))))=>n(n((D=>n(B)))))))))), poi_001238_nanbi2d, 1).
poi_theorem(nanbi12d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n(n((B=>n(D))))=>n(n((C=>n(E)))))=>n((n(n((C=>n(E))))=>n(n((B=>n(D))))))))))), poi_001239_nanbi12d, 1).
poi_theorem(nanass, n(((n(((A=>B)=>n((B=>A))))=>n(((n(n((n(n((A=>n(C))))=>n(B))))=>n(n((A=>n(n(n((C=>n(B)))))))))=>n((n(n((A=>n(n(n((C=>n(B))))))))=>n(n((n(n((A=>n(C))))=>n(B)))))))))=>n((n(((n(n((n(n((A=>n(C))))=>n(B))))=>n(n((A=>n(n(n((C=>n(B)))))))))=>n((n(n((A=>n(n(n((C=>n(B))))))))=>n(n((n(n((A=>n(C))))=>n(B))))))))=>n(((A=>B)=>n((B=>A)))))))), poi_001240_nanass, 1).
poi_theorem(xnor, n(((n(((A=>B)=>n((B=>A))))=>n(n(n(((A=>B)=>n((B=>A)))))))=>n((n(n(n(((A=>B)=>n((B=>A))))))=>n(((A=>B)=>n((B=>A)))))))), poi_001241_xnor, 0).
poi_theorem(xorcom, n(((n(n(((A=>B)=>n((B=>A)))))=>n(n(((B=>A)=>n((A=>B))))))=>n((n(n(((B=>A)=>n((A=>B)))))=>n(n(((A=>B)=>n((B=>A))))))))), poi_001242_xorcom, 0).
poi_theorem(xorass, n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(n(((A=>n(n(((B=>C)=>n((C=>B))))))=>n((n(n(((B=>C)=>n((C=>B)))))=>A))))))=>n((n(n(((A=>n(n(((B=>C)=>n((C=>B))))))=>n((n(n(((B=>C)=>n((C=>B)))))=>A)))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001243_xorass, 1).
poi_theorem(excxor, n(((n(n(((A=>B)=>n((B=>A)))))=>(n(n((A=>n(n(B)))))=>n((n(A)=>n(B)))))=>n(((n(n((A=>n(n(B)))))=>n((n(A)=>n(B))))=>n(n(((A=>B)=>n((B=>A))))))))), poi_001244_excxor, 0.56).
poi_theorem(xornan, (n(n(((A=>B)=>n((B=>A)))))=>n(n((A=>n(B))))), poi_001245_xornan, 0.11).
poi_theorem(xorneg2, n(((n(n(((A=>n(B))=>n((n(B)=>A)))))=>n(n(n(((A=>B)=>n((B=>A)))))))=>n((n(n(n(((A=>B)=>n((B=>A))))))=>n(n(((A=>n(B))=>n((n(B)=>A))))))))), poi_001246_xorneg2, 1).
poi_theorem(xorneg1, n(((n(n(((n(A)=>B)=>n((B=>n(A))))))=>n(n(n(((A=>B)=>n((B=>A)))))))=>n((n(n(n(((A=>B)=>n((B=>A))))))=>n(n(((n(A)=>B)=>n((B=>n(A)))))))))), poi_001247_xorneg1, 0.78).
poi_theorem(xorneg, n(((n(n(((n(A)=>n(B))=>n((n(B)=>n(A))))))=>n(n(((A=>B)=>n((B=>A))))))=>n((n(n(((A=>B)=>n((B=>A)))))=>n(n(((n(A)=>n(B))=>n((n(B)=>n(A)))))))))), poi_001248_xorneg, 0.56).
poi_theorem(xorbi12i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>n(((n(n(((A=>C)=>n((C=>A)))))=>n(n(((B=>D)=>n((D=>B))))))=>n((n(n(((B=>D)=>n((D=>B)))))=>n(n(((A=>C)=>n((C=>A))))))))))), poi_001249_xorbi12i, 1).
poi_theorem(xorbi12d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>(A=>n(((n(n(((B=>D)=>n((D=>B)))))=>n(n(((C=>E)=>n((E=>C))))))=>n((n(n(((C=>E)=>n((E=>C)))))=>n(n(((B=>D)=>n((D=>B)))))))))))), poi_001250_xorbi12d, 1).
poi_theorem(norcom, n(((n((n(A)=>B))=>n((n(B)=>A)))=>n((n((n(B)=>A))=>n((n(A)=>B)))))), poi_001251_norcom, 0).
poi_theorem(nornot, n(((n(A)=>n((n(A)=>A)))=>n((n((n(A)=>A))=>n(A))))), poi_001252_nornot, 0).
poi_theorem(noran, n(((n((A=>n(B)))=>n((n(n((n(A)=>A)))=>n((n(B)=>B)))))=>n((n((n(n((n(A)=>A)))=>n((n(B)=>B))))=>n((A=>n(B))))))), poi_001253_noran, 0.22).
poi_theorem(noror, n((((n(A)=>B)=>n((n(n((n(A)=>B)))=>n((n(A)=>B)))))=>n((n((n(n((n(A)=>B)))=>n((n(A)=>B))))=>(n(A)=>B))))), poi_001254_noror, 0).
poi_theorem(norasslem1, n(((((n(A)=>B)=>C)=>(n(n((n(A)=>B)))=>C))=>n(((n(n((n(A)=>B)))=>C)=>((n(A)=>B)=>C))))), poi_001255_norasslem1, 0).
poi_theorem(norasslem2, (A=>n(((B=>((n(A)=>C)=>B))=>n((((n(A)=>C)=>B)=>B))))), poi_001256_norasslem2, 0).
poi_theorem(norasslem3, (n(A)=>n((((B=>C)=>((n(A)=>B)=>C))=>n((((n(A)=>B)=>C)=>(B=>C)))))), poi_001257_norasslem3, 0.11).
poi_theorem(norass, n(((n(((A=>B)=>n((B=>A))))=>n(((n((n(n((n(A)=>C)))=>B))=>n((n(A)=>n((n(C)=>B)))))=>n((n((n(A)=>n((n(C)=>B))))=>n((n(n((n(A)=>C)))=>B)))))))=>n((n(((n((n(n((n(A)=>C)))=>B))=>n((n(A)=>n((n(C)=>B)))))=>n((n((n(A)=>n((n(C)=>B))))=>n((n(n((n(A)=>C)))=>B))))))=>n(((A=>B)=>n((B=>A)))))))), poi_001258_norass, 1).
poi_theorem('pm2.21fal', ((A=>B)=>((A=>n(B))=>(A=>falsehood))), 'poi_001259_pm2.21fal', 0).
poi_theorem(nottru, n(((n(truth)=>n(truth))=>n((n(truth)=>n(truth))))), poi_001260_nottru, 0).
poi_theorem(truantru, n(((n((truth=>n(truth)))=>truth)=>n((truth=>n((truth=>n(truth))))))), poi_001261_truantru, 0).
poi_theorem(falanfal, n(((n((falsehood=>n(falsehood)))=>falsehood)=>n((falsehood=>n((falsehood=>n(falsehood))))))), poi_001262_falanfal, 0).
poi_theorem(truortru, n((((n(truth)=>truth)=>truth)=>n((truth=>(n(truth)=>truth))))), poi_001263_truortru, 0).
poi_theorem(falorfal, n((((n(falsehood)=>falsehood)=>falsehood)=>n((falsehood=>(n(falsehood)=>falsehood))))), poi_001264_falorfal, 0).
poi_theorem(trunantru, n(((n(n((truth=>n(truth))))=>n(truth))=>n((n(truth)=>n(n((truth=>n(truth)))))))), poi_001265_trunantru, 0).
poi_theorem(trunortru, n(((n((n(truth)=>truth))=>n(truth))=>n((n(truth)=>n((n(truth)=>truth)))))), poi_001266_trunortru, 0).
poi_theorem(hadbi123d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>((A=>n(((F=>G)=>n((G=>F)))))=>(A=>n(((n(n(((n(n(((B=>D)=>n((D=>B)))))=>F)=>n((F=>n(n(((B=>D)=>n((D=>B))))))))))=>n(n(((n(n(((C=>E)=>n((E=>C)))))=>G)=>n((G=>n(n(((C=>E)=>n((E=>C)))))))))))=>n((n(n(((n(n(((C=>E)=>n((E=>C)))))=>G)=>n((G=>n(n(((C=>E)=>n((E=>C))))))))))=>n(n(((n(n(((B=>D)=>n((D=>B)))))=>F)=>n((F=>n(n(((B=>D)=>n((D=>B)))))))))))))))))), poi_001267_hadbi123d, 1).
poi_theorem(hadbi123i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>(n(((E=>F)=>n((F=>E))))=>n(((n(n(((n(n(((A=>C)=>n((C=>A)))))=>E)=>n((E=>n(n(((A=>C)=>n((C=>A))))))))))=>n(n(((n(n(((B=>D)=>n((D=>B)))))=>F)=>n((F=>n(n(((B=>D)=>n((D=>B)))))))))))=>n((n(n(((n(n(((B=>D)=>n((D=>B)))))=>F)=>n((F=>n(n(((B=>D)=>n((D=>B))))))))))=>n(n(((n(n(((A=>C)=>n((C=>A)))))=>E)=>n((E=>n(n(((A=>C)=>n((C=>A))))))))))))))))), poi_001268_hadbi123i, 1).
poi_theorem(hadbi, n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(((n(((A=>B)=>n((B=>A))))=>C)=>n((C=>n(((A=>B)=>n((B=>A)))))))))=>n((n(((n(((A=>B)=>n((B=>A))))=>C)=>n((C=>n(((A=>B)=>n((B=>A))))))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001269_hadbi, 1).
poi_theorem(hadcoma, n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(n(((n(n(((B=>A)=>n((A=>B)))))=>C)=>n((C=>n(n(((B=>A)=>n((A=>B)))))))))))=>n((n(n(((n(n(((B=>A)=>n((A=>B)))))=>C)=>n((C=>n(n(((B=>A)=>n((A=>B))))))))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001270_hadcoma, 1).
poi_theorem(hadcomb, n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(n(((n(n(((A=>C)=>n((C=>A)))))=>B)=>n((B=>n(n(((A=>C)=>n((C=>A)))))))))))=>n((n(n(((n(n(((A=>C)=>n((C=>A)))))=>B)=>n((B=>n(n(((A=>C)=>n((C=>A))))))))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001271_hadcomb, 1).
poi_theorem(hadrot, n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(n(((n(n(((B=>C)=>n((C=>B)))))=>A)=>n((A=>n(n(((B=>C)=>n((C=>B)))))))))))=>n((n(n(((n(n(((B=>C)=>n((C=>B)))))=>A)=>n((A=>n(n(((B=>C)=>n((C=>B))))))))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001272_hadrot, 1).
poi_theorem(hadnot, n(((n(n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))=>n(n(((n(n(((n(A)=>n(B))=>n((n(B)=>n(A))))))=>n(C))=>n((n(C)=>n(n(((n(A)=>n(B))=>n((n(B)=>n(A))))))))))))=>n((n(n(((n(n(((n(A)=>n(B))=>n((n(B)=>n(A))))))=>n(C))=>n((n(C)=>n(n(((n(A)=>n(B))=>n((n(B)=>n(A)))))))))))=>n(n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))))))), poi_001273_hadnot, 1).
poi_theorem(had1, (A=>n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(((B=>C)=>n((C=>B)))))=>n((n(((B=>C)=>n((C=>B))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))))))), poi_001274_had1, 1).
poi_theorem(had0, (n(A)=>n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>n(n(((B=>C)=>n((C=>B))))))=>n((n(n(((B=>C)=>n((C=>B)))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))))))), poi_001275_had0, 1).
poi_theorem(hadifp, n(((n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A))))))))))=>(n(n((A=>n(n(((B=>C)=>n((C=>B))))))))=>n((n(A)=>n(n(n(((B=>C)=>n((C=>B))))))))))=>n(((n(n((A=>n(n(((B=>C)=>n((C=>B))))))))=>n((n(A)=>n(n(n(((B=>C)=>n((C=>B)))))))))=>n(n(((n(n(((A=>B)=>n((B=>A)))))=>C)=>n((C=>n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001276_hadifp, 1).
poi_theorem(cador, n((((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))=>(n((n(n((A=>n(B))))=>n((A=>n(C)))))=>n((B=>n(C)))))=>n(((n((n(n((A=>n(B))))=>n((A=>n(C)))))=>n((B=>n(C))))=>(n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))))), poi_001277_cador, 1).
poi_theorem(cadan, n((((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))=>n((n(((n(A)=>B)=>n((n(A)=>C))))=>n((n(B)=>C)))))=>n((n((n(((n(A)=>B)=>n((n(A)=>C))))=>n((n(B)=>C))))=>(n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))))), poi_001278_cadan, 1).
poi_theorem(cadbi123d, ((A=>n(((B=>C)=>n((C=>B)))))=>((A=>n(((D=>E)=>n((E=>D)))))=>((A=>n(((F=>G)=>n((G=>F)))))=>(A=>n((((n(n((B=>n(D))))=>n((F=>n(n(n(((B=>D)=>n((D=>B)))))))))=>(n(n((C=>n(E))))=>n((G=>n(n(n(((C=>E)=>n((E=>C))))))))))=>n(((n(n((C=>n(E))))=>n((G=>n(n(n(((C=>E)=>n((E=>C)))))))))=>(n(n((B=>n(D))))=>n((F=>n(n(n(((B=>D)=>n((D=>B))))))))))))))))), poi_001279_cadbi123d, 1).
poi_theorem(cadbi123i, (n(((A=>B)=>n((B=>A))))=>(n(((C=>D)=>n((D=>C))))=>(n(((E=>F)=>n((F=>E))))=>n((((n(n((A=>n(C))))=>n((E=>n(n(n(((A=>C)=>n((C=>A)))))))))=>(n(n((B=>n(D))))=>n((F=>n(n(n(((B=>D)=>n((D=>B))))))))))=>n(((n(n((B=>n(D))))=>n((F=>n(n(n(((B=>D)=>n((D=>B)))))))))=>(n(n((A=>n(C))))=>n((E=>n(n(n(((A=>C)=>n((C=>A)))))))))))))))), poi_001280_cadbi123i, 1).
poi_theorem(cadcoma, n((((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))=>(n(n((B=>n(A))))=>n((C=>n(n(n(((B=>A)=>n((A=>B))))))))))=>n(((n(n((B=>n(A))))=>n((C=>n(n(n(((B=>A)=>n((A=>B)))))))))=>(n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))))), poi_001281_cadcoma, 0.67).
poi_theorem(cadcomb, n((((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))=>(n(n((A=>n(C))))=>n((B=>n(n(n(((A=>C)=>n((C=>A))))))))))=>n(((n(n((A=>n(C))))=>n((B=>n(n(n(((A=>C)=>n((C=>A)))))))))=>(n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))))), poi_001282_cadcomb, 1).
poi_theorem(cadrot, n((((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))=>(n(n((B=>n(C))))=>n((A=>n(n(n(((B=>C)=>n((C=>B))))))))))=>n(((n(n((B=>n(C))))=>n((A=>n(n(n(((B=>C)=>n((C=>B)))))))))=>(n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))))), poi_001283_cadrot, 1).
poi_theorem(cadnot, n(((n((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))=>(n(n((n(A)=>n(n(B)))))=>n((n(C)=>n(n(n(((n(A)=>n(B))=>n((n(B)=>n(A)))))))))))=>n(((n(n((n(A)=>n(n(B)))))=>n((n(C)=>n(n(n(((n(A)=>n(B))=>n((n(B)=>n(A))))))))))=>n((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))))))), poi_001284_cadnot, 1).
poi_theorem(cad1, (A=>n((((n(n((B=>n(C))))=>n((A=>n(n(n(((B=>C)=>n((C=>B)))))))))=>(n(B)=>C))=>n(((n(B)=>C)=>(n(n((B=>n(C))))=>n((A=>n(n(n(((B=>C)=>n((C=>B)))))))))))))), poi_001285_cad1, 1).
poi_theorem(cadifp, n((((n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A)))))))))=>(n(n((C=>n((n(A)=>B)))))=>n((n(C)=>n(n((A=>n(B))))))))=>n(((n(n((C=>n((n(A)=>B)))))=>n((n(C)=>n(n((A=>n(B)))))))=>(n(n((A=>n(B))))=>n((C=>n(n(n(((A=>B)=>n((B=>A))))))))))))), poi_001286_cadifp, 1).
poi_theorem(minimp, (_=>((A=>B)=>(((_=>A)=>(B=>C))=>(A=>C)))), poi_001287_minimp, 0).
poi_theorem('minimp-ax1', (A=>(_=>A)), 'poi_001288_minimp-ax1', 0).
poi_theorem('minimp-ax2c', ((A=>B)=>((A=>(B=>C))=>(A=>C))), 'poi_001289_minimp-ax2c', 0).
poi_theorem('minimp-ax2', ((A=>(B=>C))=>((A=>B)=>(A=>C))), 'poi_001290_minimp-ax2', 0).
poi_theorem(impsingle, (((A=>_)=>B)=>((B=>A)=>(_=>A))), poi_001291_impsingle, 0.33).
poi_theorem('impsingle-step4', (((A=>_)=>A)=>(_=>A)), 'poi_001292_impsingle-step4', 0).
poi_theorem('impsingle-step15', (((A=>_)=>(B=>C))=>((A=>C)=>(B=>C))), 'poi_001293_impsingle-step15', 0.11).
poi_theorem('impsingle-step18', ((((A=>B)=>(_=>B))=>(((B=>C)=>A)=>D))=>(_=>(((B=>C)=>A)=>D))), 'poi_001294_impsingle-step18', 0.33).
poi_theorem('impsingle-step19', ((((A=>B)=>C)=>(D=>B))=>(((B=>C)=>D)=>(A=>B))), 'poi_001295_impsingle-step19', 0.44).
poi_theorem('impsingle-step20', ((((A=>B)=>B)=>(C=>B))=>(((B=>_)=>A)=>(C=>B))), 'poi_001296_impsingle-step20', 0).
poi_theorem('impsingle-step21', ((((A=>B)=>C)=>C)=>((C=>B)=>(A=>B))), 'poi_001297_impsingle-step21', 0.33).
poi_theorem('impsingle-step25', ((A=>B)=>(((A=>_)=>B)=>B)), 'poi_001298_impsingle-step25', 0.11).
poi_theorem(meredith, (((((A=>_)=>(n(B)=>n(C)))=>B)=>D)=>((D=>A)=>(C=>A))), poi_001299_meredith, 0.78).
poi_theorem(merlem1, (((_=>(n(A)=>_))=>B)=>(A=>B)), poi_001300_merlem1, 0).
poi_theorem(merlem2, (((A=>A)=>B)=>(_=>B)), poi_001301_merlem2, 0).
poi_theorem(merlem4, (A=>((A=>B)=>(_=>B))), poi_001302_merlem4, 0).
poi_theorem(merlem5, ((A=>B)=>(n(n(A))=>B)), poi_001303_merlem5, 0).
poi_theorem(merlem6, (A=>(((_=>A)=>B)=>(_=>B))), poi_001304_merlem6, 0).
poi_theorem(merlem7, (_=>(((A=>B)=>C)=>(((B=>_)=>(n(C)=>n(A)))=>C))), poi_001305_merlem7, 0.33).
poi_theorem(merlem8, (((A=>B)=>C)=>(((B=>_)=>(n(C)=>n(A)))=>C)), poi_001306_merlem8, 0.56).
poi_theorem(merlem9, (((_=>A)=>(B=>(C=>(A=>D))))=>(_=>(B=>(C=>(A=>D))))), poi_001307_merlem9, 0).
poi_theorem(merlem10, ((A=>(A=>B))=>(_=>(A=>B))), poi_001308_merlem10, 0).
poi_theorem(merlem12, (((_=>(n(n(A))=>A))=>B)=>B), poi_001309_merlem12, 0).
poi_theorem(merlem13, ((A=>B)=>(((_=>(n(n(C))=>C))=>n(n(A)))=>B)), poi_001310_merlem13, 0).
poi_theorem(luklem2, ((A=>n(B))=>(((A=>_)=>C)=>(B=>C))), poi_001311_luklem2, 0.11).
poi_theorem(luklem3, (A=>(((n(A)=>_)=>B)=>(_=>B))), poi_001312_luklem3, 0).
poi_theorem(luklem4, ((((n(A)=>A)=>A)=>B)=>B), poi_001313_luklem4, 0).
poi_theorem('nic-dfim', n(n((n(n((n(n((A=>n(n(n((B=>n(B))))))))=>n((A=>B)))))=>n(n(n((n(n((n(n((A=>n(n(n((B=>n(B))))))))=>n(n(n((A=>n(n(n((B=>n(B))))))))))))=>n(n(n(((A=>B)=>n((A=>B))))))))))))), 'poi_001314_nic-dfim', 0.33).
poi_theorem('nic-dfneg', n(n((n(n((n(n((A=>n(A))))=>n(n(A)))))=>n(n(n((n(n((n(n((A=>n(A))))=>n(n(n((A=>n(A))))))))=>n(n(n((n(A)=>n(n(A))))))))))))), 'poi_001315_nic-dfneg', 0).
poi_theorem('nic-mp', (A=>(n(n((A=>n(n(n((_=>n(B))))))))=>B)), 'poi_001316_nic-mp', 0).
poi_theorem('nic-ax', n(n((n(n((A=>n(n(n((B=>n(_))))))))=>n(n(n((n(n((C=>n(n(n((C=>n(C))))))))=>n(n(n((n(n((D=>n(B))))=>n(n(n((n(n((A=>n(D))))=>n(n(n((A=>n(D)))))))))))))))))))), 'poi_001317_nic-ax', 0.78).
poi_theorem('nic-imp', (n(n((A=>n(n(n((B=>n(_))))))))=>n(n((n(n((C=>n(B))))=>n(n(n((n(n((A=>n(C))))=>n(n(n((A=>n(C))))))))))))), 'poi_001318_nic-imp', 0.78).
poi_theorem('nic-idlem1', n(n((n(n((A=>n(n(n((B=>n(n(n((B=>n(B))))))))))))=>n(n(n((n(n((n(n((C=>n(n(n((D=>n(E))))))))=>n(A))))=>n(n(n((n(n((C=>n(n(n((D=>n(E))))))))=>n(A)))))))))))), 'poi_001319_nic-idlem1', 0.11).
poi_theorem('nic-idlem2', (n(n((A=>n(n(n((n(n((_=>n(n(n((_=>n(_))))))))=>n(B))))))))=>n(n((n(n((B=>n(n(n((C=>n(n(n((C=>n(C))))))))))))=>n(A))))), 'poi_001320_nic-idlem2', 0.22).
poi_theorem('nic-id', n(n((A=>n(n(n((A=>n(A)))))))), 'poi_001321_nic-id', 0).
poi_theorem('nic-swap', n(n((n(n((A=>n(B))))=>n(n(n((n(n((B=>n(A))))=>n(n(n((B=>n(A)))))))))))), 'poi_001322_nic-swap', 0).
poi_theorem('nic-isw1', (n(n((A=>n(B))))=>n(n((B=>n(A))))), 'poi_001323_nic-isw1', 0).
poi_theorem('nic-isw2', (n(n((A=>n(n(n((B=>n(C))))))))=>n(n((A=>n(n(n((C=>n(B))))))))), 'poi_001324_nic-isw2', 0).
poi_theorem('nic-iimp1', (n(n((A=>n(n(n((B=>n(_))))))))=>(n(n((C=>n(B))))=>n(n((C=>n(A)))))), 'poi_001325_nic-iimp1', 0.11).
poi_theorem('nic-iimp2', (n(n((n(n((A=>n(_))))=>n(n(n((B=>n(B))))))))=>(n(n((C=>n(A))))=>n(n((C=>n(n(n((B=>n(B)))))))))), 'poi_001326_nic-iimp2', 0.33).
poi_theorem('nic-idel', (n(n((A=>n(n(n((B=>n(_))))))))=>n(n((A=>n(n(n((B=>n(B))))))))), 'poi_001327_nic-idel', 0).
poi_theorem('nic-ich', (n(n((A=>n(n(n((B=>n(B))))))))=>(n(n((B=>n(n(n((C=>n(C))))))))=>n(n((A=>n(n(n((C=>n(C)))))))))), 'poi_001328_nic-ich', 0.33).
poi_theorem('nic-idbl', (n(n((A=>n(n(n((B=>n(B))))))))=>n(n((n(n((B=>n(B))))=>n(n(n((n(n((A=>n(A))))=>n(n(n((A=>n(A))))))))))))), 'poi_001329_nic-idbl', 0.11).
poi_theorem('nic-bijust', n(n((n(n((A=>n(A))))=>n(n(n((n(n((A=>n(A))))=>n(n(n((A=>n(A)))))))))))), 'poi_001330_nic-bijust', 0).
poi_theorem('nic-bi1', (n(n((n(n((A=>n(B))))=>n(n(n((n(n((A=>n(A))))=>n(n(n((B=>n(B))))))))))))=>n(n((A=>n(n(n((B=>n(B))))))))), 'poi_001331_nic-bi1', 0.11).
poi_theorem('nic-bi2', (n(n((n(n((A=>n(B))))=>n(n(n((n(n((A=>n(A))))=>n(n(n((B=>n(B))))))))))))=>n(n((B=>n(n(n((A=>n(A))))))))), 'poi_001332_nic-bi2', 0.11).
poi_theorem('lukshef-ax1', n(n((n(n((A=>n(n(n((B=>n(_))))))))=>n(n(n((n(n((C=>n(n(n((C=>n(C))))))))=>n(n(n((n(n((C=>n(B))))=>n(n(n((n(n((A=>n(C))))=>n(n(n((A=>n(C)))))))))))))))))))), 'poi_001333_lukshef-ax1', 0.78).
poi_theorem(lukshefth1, n(n((n(n((n(n((n(n((A=>n(B))))=>n(n(n((n(n((C=>n(A))))=>n(n(n((C=>n(A))))))))))))=>n(n(n((D=>n(n(n((D=>n(D))))))))))))=>n(n(n((C=>n(n(n((B=>n(_)))))))))))), poi_001334_lukshefth1, 0.78).
poi_theorem(tbwlem3, (((((A=>falsehood)=>A)=>A)=>B)=>B), poi_001335_tbwlem3, 0).
poi_theorem(merco1lem7, (_=>(((A=>_)=>A)=>A)), poi_001336_merco1lem7, 0).
poi_theorem(merco1lem8, (_=>((A=>(A=>B))=>(A=>B))), poi_001337_merco1lem8, 0).
poi_theorem(merco1lem10, (((((A=>_)=>B)=>(_=>B))=>A)=>(_=>A)), poi_001338_merco1lem10, 0).
poi_theorem(merco1lem12, ((A=>B)=>(((_=>(A=>_))=>A)=>B)), poi_001339_merco1lem12, 0.11).
poi_theorem(merco1lem13, ((((A=>B)=>(_=>B))=>C)=>(A=>C)), poi_001340_merco1lem13, 0).
poi_theorem(merco1lem14, ((((A=>B)=>B)=>C)=>(A=>C)), poi_001341_merco1lem14, 0).
poi_theorem(merco1lem15, ((A=>B)=>(A=>(_=>B))), poi_001342_merco1lem15, 0).
poi_theorem(merco1lem16, (((A=>(_=>B))=>C)=>((A=>B)=>C)), poi_001343_merco1lem16, 0).
poi_theorem(merco1lem17, (((((A=>_)=>A)=>B)=>C)=>((A=>B)=>C)), poi_001344_merco1lem17, 0.11).
poi_theorem(merco1lem18, ((A=>(B=>C))=>((B=>A)=>(B=>C))), poi_001345_merco1lem18, 0).
poi_theorem(mercolem1, (((_=>A)=>B)=>(A=>(_=>B))), poi_001346_mercolem1, 0).
poi_theorem(mercolem2, (((A=>_)=>A)=>(_=>(_=>A))), poi_001347_mercolem2, 0).
poi_theorem(mercolem4, ((A=>(B=>C))=>(((A=>_)=>C)=>(_=>(B=>C)))), poi_001348_mercolem4, 0).
poi_theorem(mercolem5, (A=>((A=>B)=>(_=>(_=>B)))), poi_001349_mercolem5, 0).
poi_theorem(mercolem6, ((A=>(B=>(A=>C)))=>(B=>(A=>C))), poi_001350_mercolem6, 0).
poi_theorem(mercolem7, ((A=>B)=>(((A=>_)=>(C=>B))=>(C=>B))), poi_001351_mercolem7, 0.11).
poi_theorem(mercolem8, ((A=>B)=>((B=>(A=>C))=>(_=>(_=>(A=>C))))), poi_001352_mercolem8, 0).
poi_theorem('rb-bijust', n(((n(((A=>B)=>n((B=>A))))=>n((n(n((n(n(A))=>B)))=>n((n(n(B))=>A)))))=>n((n((n(n((n(n(A))=>B)))=>n((n(n(B))=>A))))=>n(((A=>B)=>n((B=>A)))))))), 'poi_001353_rb-bijust', 0.56).
poi_theorem('rb-imdf', n((n(n((n(n((A=>B)))=>(n(n(A))=>B))))=>n((n(n((n(n(A))=>B)))=>(A=>B))))), 'poi_001354_rb-imdf', 0).
poi_theorem(anmp, (A=>((n(n(A))=>B)=>B)), poi_001355_anmp, 0).
poi_theorem('rb-ax1', (n(n((n(n(A))=>B)))=>(n(n((n(C)=>A)))=>(n(C)=>B))), 'poi_001356_rb-ax1', 0.11).
poi_theorem('rb-ax2', (n(n((n(A)=>B)))=>(n(B)=>A)), 'poi_001357_rb-ax2', 0).
poi_theorem('rb-ax3', (n(n(A))=>(n(_)=>A)), 'poi_001358_rb-ax3', 0).
poi_theorem('rb-ax4', (n(n((n(A)=>A)))=>A), 'poi_001359_rb-ax4', 0).
poi_theorem(rbsyl, ((n(n(A))=>B)=>((n(C)=>A)=>(n(C)=>B))), poi_001360_rbsyl, 0).
poi_theorem(rblem1, ((n(n(A))=>B)=>((n(n(C))=>D)=>(n(n((n(A)=>C)))=>(n(B)=>D)))), poi_001361_rblem1, 0.89).
poi_theorem(rblem2, (n(n((n(A)=>B)))=>(n(A)=>(n(B)=>_))), poi_001362_rblem2, 0).
poi_theorem(rblem3, (n(n((n(A)=>B)))=>(n((n(A)=>_))=>B)), poi_001363_rblem3, 0).
poi_theorem(rblem4, ((n(n(A))=>B)=>((n(n(C))=>D)=>((n(n(E))=>F)=>(n(n((n((n(A)=>C))=>E)))=>(n((n(F)=>D))=>B))))), poi_001364_rblem4, 1).
poi_theorem(rblem5, (n(n((n(n(n(A)))=>B)))=>(n(n(n(B)))=>A)), poi_001365_rblem5, 0).
poi_theorem(rblem6, (n((n(n((n(n(A))=>B)))=>n((n(n(B))=>A))))=>(n(n(A))=>B)), poi_001366_rblem6, 0).
poi_theorem(rblem7, (n((n(n((n(n(A))=>B)))=>n((n(n(B))=>A))))=>(n(n(B))=>A)), poi_001367_rblem7, 0).
poi_theorem(mptnan, (A=>(n(n((A=>n(B))))=>n(B))), poi_001368_mptnan, 0).
poi_theorem(mptxor, (A=>(n(n(((A=>B)=>n((B=>A)))))=>n(B))), poi_001369_mptxor, 0.11).
poi_theorem(mtpxor, (n(A)=>(n(n(((A=>B)=>n((B=>A)))))=>B)), poi_001370_mtpxor, 0.11).
poi_theorem(stoic1b, ((n((A=>n(B)))=>C)=>(n((B=>n(n(C))))=>n(A))), poi_001371_stoic1b, 0.11).
poi_theorem(stoic3, ((n((A=>n(B)))=>C)=>((n((C=>n(D)))=>E)=>(n((n((A=>n(B)))=>n(D)))=>E))), poi_001372_stoic3, 1).
poi_theorem(stoic4a, ((n((A=>n(B)))=>C)=>((n((n((C=>n(A)))=>n(D)))=>E)=>(n((n((A=>n(B)))=>n(D)))=>E))), poi_001373_stoic4a, 1).
poi_theorem(stoic4b, ((n((A=>n(B)))=>C)=>((n((n((n((C=>n(A)))=>n(B)))=>n(D)))=>E)=>(n((n((A=>n(B)))=>n(D)))=>E))), poi_001374_stoic4b, 1).