Definition - d--1:

a	;
("p and q are simultaneous satisfied")	;

 Definition - d--2:

b	;
("p and not-q are simultaneous satisfied")	;

 Definition - d--3:

c	;
("not-p and q are simultaneous satisfied")	;

 Definition - d--4:

d	;
("not-p and not-q are simultaneous satisfied")	;

 Definition - d--5:

~p	;
c + d	;

 Definition - d--6:

(p&q)	;
a	;

 Definition - d--7:

(p&~q)	;
b	;

 Definition - d--8:

(~p&q)	;
c	;

 Definition - d--9:

(~p&~q)	;
d	;

 Definition - d--10:

(p xor q)	;
b + c	;

 Definition - d--11:

(p<->q)	;
a + d	;

 Definition - d--12:

(pvq)	;
a + b + c	;

 Definition - d--13:

(p->q)	;
a + c + d	;

 Definition - d--14:

(p=>q)	;
a / (a + b)	;

 Definition - d--15:

(p<=>q)	;
a / (a + b + c)	;

 Definition - d--16:

A(p,q)	;
(ad-bc)	;

 Definition - d--17:

Tp	;
(p=1)	;

 Definition - d--18:

Fp	;
(p<>1)	;

 Definition - d--19:

Ep	;
(p<>0)	;

 Definition - d--20:

Up	;
(p=0)	;

 Definition - d--21:

Lp	;
(p==1)	;

 Definition - d--22:

Mp	;
~(p==0)	;

 Axiom - a--23:

(p&q)	;
(q&p)	;

 Axiom - a--24:

(p&~p)	;
0	;

 Axiom - a--25:

(p&1)	;
p	;

 Axiom - a--26:

((p&q)&r)	;
(p&q&r)	;

 Axiom - a--27:

1	;
p + ~p	;

 Axiom - a--28:

1	;
a + b + c + d	;

 Proof - t--29:

p	;
p + ~p - ~p	; expand
1 - ~p	; a--23

 Proof - t--30:

~p	;
~p + p - p	; expand
1 - p	; a--23

 Proof - t--31:

~~p	;
~(~p)	; rearrange
1 - (1 - p)	; t--30, t--30
1 - 1 + p	; rearrange
p	; reduce

 Proof - t--32:

~0	;
1 - 0	; t--30
1	; reduce

 Proof - t--33:

~1	;
1-1	; t--30
0	; reduce

 Proof - t--34:

p	;
1 - ~p	; t--29
(a + b + c + d) - (c + d)	; a--28, d--5
a + b	; reduce

 Proof - t--35:

p	;
a + b	; t--34
(p&q) + (p&~q)	; d--6, d--7

 Proof - t--36:

q	;
(q&p) + (q&~p)	; d--6, d--7
(p&q) + (~p&q)	; a--23, a--23

 Proof - t--37:

q	;
(p&q) + (~p&q)	; t--36
a + c	; d--6, d--8

 Proof - t--38:

~p	;
(~p&q) + (~p&~q)	; t--35

 Proof - t--39:

~q	;
(p&~q) + (~p&~q)	; t--36

 Proof - t--40:

(p xor q)	;
b + c	; d--11
(p&~q) + (~p&q)	; d--7, d--8

 Proof - t--41:

(p <-> q)	;
a + d	; d--12
(p&q) + (~p&~q)	; d--6, d--9

 Proof - t--42:

(p -> q)	;
a + c + d	; d--14
(p&q) + (~p&q) + (~p&~q)	; d--6, d--8, d--9

 Proof - t--43:

(q -> p)	;
(q&p) + (~q&p) + (~q&~p)	; t--42
(p&q) + (p&~q) + (~p&~q)	; a--23, a--23, a--23

 Proof - t--44:

(pvq)	;
a + b + c	; d--13
(p&q) + (p&~q) + (~p&q)	; d--6, d--7, d--8

 Proof - t--45:

(p => q)	;
a / (a + b)	; d--15
(p&q) / ((p&q) + (p&~q))	; d--6, d--6, d--7

 Proof - t--46:

(q => p)	;
(q&p) / ((q&p) + (q&~p))	; t--45
(p&q) / ((p&q) + (~p&q))	; a--23, a--23, a--23

 Proof - t--47:

(p <=> q)	;
a / (a + b + c)	; d--16
(p&q) / ((p&q) + (p&~q) + (~p&q))	; d--6, d--6, d--7, d--8

 Proof - t--48:

(ad-bc)	;
(p&q)(~p&~q) - (p&~q)(~p&q)	; d--6, d--9, d--7, d--8

 Proof - t--49:

A(p,q)	;
(ad-bc)	; d--17
(p&q)(~p&~q) - (p&~q)(~p&q)	; t--48

 Proof - t--50:

~q	;
(p&~q) + (~p&~q)	; t--39
b + d	; d--7, d--9

 Proof - t--51:

(pv~q)	;
(p&~q) + (p&~~q) + (~p&~q)	; t--44
(p&~q) + (p&q) + (~p&~q)	; t--31
b + a + d	; d--7, d--6, d--9
a + b + d	; rearrange

 Proof - t--52:

(~pvq)	;
(~p&q) + (~p&~q) + (~~p&q)	; t--44
(~p&q) + (~p&~q) + (p&q)	; t--31
c + d + a	; d--8, d--9, d--6
a + c + d	; rearrange

 Proof - t--53:

(~pv~q)	;
(~p&~q) + (~p&~~q) + (~~p&~q)	; t--52
(~p&~q) + (~p&q) + (p&~q)	; t--31
d + c + b	; d--9, d--8, d--7
b + c + d	; rearrange

 Proof - t--54:

(q -> p)	;
(p&q) + (p&~q) + (~p&~q)	; t--43
a + b + d	; d--6, d--7, d--9

 Proof - t--55:

(q => p)	;
(p&q) / ((p&q) + (~p&q))	; t--46
a / (a + c)	; d--6, d--6, d--8

 Proof - t--56:

(p -> q)	;
a + c + d	; d--14
(~pvq)	; t--52

 Proof - t--57:

(p -> q)	;
a + c + d	; d--14
a + c + d + 1 - 1	; expand
a + c + d + 1 - (a+b+c+d)	; a--28
1 - b	; reduce
~(p&~q)	; t--30, d--7

 Proof - t--58:

(p <-> q)	;
a + d	; d--12
a + d + 1 - 1	; expand
a + d + 1 - (a+b+c+d)	; a--28
1 - (b+c)	; reduce
~(p xor q)	; t--30, d--11

 Proof - t--59:

(p => q)	;
a / (a + b)	; d--15
(p&q) / p	; d--6, t--34

 Proof - t--60:

(p <=> q)	;
a / (a + b + c)	; d--16
(p&q) / (pvq)	; d--6, d--13

 Proof - t--61:

(pvq)	;
a + b + c	; d--13
a + b + c + a - a	; expand
(a+b) + (a+c) - a	; rearrange
p + q - (p&q)	; t--34, t--37, d--6

 Proof - t--62:

(p -> q)	;
a + c + d	; d--14
a + c + d + b - b + a - a	; expand
(a+b+c+d) - (a+b) + a	; rearrange
1 - p + (p&q)	; a--28, t--34, d--6

 Proof - t--63:

(q -> p)	;
1 - q + (q&p)	; t--62
1 - q + (p&q)	; a--23

 Proof - t--64:

(q => p)	;
(q&p) / q	; t--59
(p&q) / q	; a--23

 Proof - t--65:

(p xor q)	;
b + c	; d--11
b + c + a - a + a - a	; expand
(a+b) + (a+c) - 2a	; rearrange
p + q - 2(p&q)	; t--34, t--37, d--6

 Proof - t--66:

(p <-> q)	;
a + d	; d--12
a + d + 2a - 2a + b - b + c - c	; expand
(a+b+c+d) - (a+b) - (a+c) + 2a	; rearrange
1 - p - q + 2(p&q)	; a--28, t--34, t--37, d--6

 Proof - t--67:

(p <=> q)	;
(p&q) / (pvq)	; t--60
(p&q) / (p + q - (p&q))	; t--61

 Proof - t--68:

(p&q)	;
a	; d--6
a + (a+b+c) - (a+b+c)	; expand
(a+b) + (a+c) - (a+b+c)	; rearrange
p + q - (pvq)	; t--34, t--37, d--13

 Proof - t--69:

A(p,~q)	;
(p&~q)(~p&~~q) - (p&~~q)(~p&~q)	; t--49
(p&~q)(~p&q) - (p&q)(~p&~q)	; t--31, t--31
bc - ad	; d--7, d--8, d--6, d--9
- (ad-bc)	; rearrange

 Proof - t--70:

A(~p,q)	;
(~p&q)(~~p&~q) - (~p&~q)(~~p&q)	; t--49
(~p&q)(p&~q) - (~p&~q)(p&q)	; t--31, t--31
cb - da	; d--8, d--7, d--9, d--6
- (ad-bc)	; rearrange

 Proof - t--71:

A(~p,~q)	;
(~p&~q)(~~p&~~q) - (~p&~~q)(~~p&~q)	; t--49
(~p&~q)(p&q) - (~p&q)(p&~q)	; t--31, t--31, t--31, t--31
da - cb	; d--9, d--6, d--8, d--7
(ad-bc)	; rearrange

 Proof - t--72:

pq	;
(a+b)(a+c)	; t--34, t--37
aa + ab + ac + bc	; rearrange
aa + ab + ac + bc + ad - ad	; expand
(aa + ab + ac + ad) - ad + bc	; rearrange
a(a+b+c+d) - ad + bc	; rearrange
a*1 - ad + bc	; a--28
a - ad + bc	; reduce

 Proof - t--73:

(p&q)	;
a	; d--6
a + ad - ad + bc - bc	; expand
(a-ad+bc) + (ad-bc)	; rearrange
pq + (ad-bc)	; t--72

 Proof - t--74:

(p&q)	;
pq + (ad-bc)	; t--73
pq + A(p,q)	; d--17

 Proof - t--75:

(pvq)	;
(p&q) + (p&~q) + (~p&q)	; t--44
(q&p) + (~q&p) + (q&~p)	; a--23, a--23, a--23
(q&p) + (q&~p) + (~q&p)	; rearrange
(qvp)	; t--44

 Proof - t--76:

(p xor q)	;
(p&~q) + (~p&q)	; t--40
(~q&p) + (q&~p)	; a--23, a--23
(q&~p) + (~q&p)	; rearrange
(q xor p)	; t--40

 Proof - t--77:

(p <-> q)	;
(p&q) + (~p&~q)	; t--41
(q&p) + (~q&~p)	; a--23, a--23
(q <-> p)	; t--41

 Proof - t--78:

(p <=> q)	;
(p&q) / (pvq)	; t--60
(q&p) / (qvp)	; t--75
(q <=> p)	; t--60

 Proof - t--79:

(p&p)	;
(p&p) + (p&~p) - (p&~p)	; expand
(p&p) + (p&~p) - 0	; a--24
p	; t--35

 Proof - t--80:

(pvp)	;
(p&p) + (p&~p) + (~p&p)	; t--44
(p&p) + (p&~p) + (p&~p)	; t--75
(p&p) + 0 + 0	; reduce
p	; t--79

 Proof - t--81:

(p -> p)	;
(~pvp)	; t--56
~p + p - (~p&p)	; t--68
~p + p - (p&~p)	; t--75
p + ~p - 0	; a--23
1	; a--27

 Proof - t--82:

(p => p)	;
(p&p) / p	; t--59
p / p	; t--79

 Proof - t--83:

(p xor p)	;
(p&~p) + (~p&p)	; t--40
(p&~p) + (p&~p)	; t--75
0 + 0	; a--24, a--24
0	; reduce

 Proof - t--84:

(p <-> p)	;
(p&p) + (~p&~p)	; t--41
p + ~p	; t--79, t--79
1	; a--23

 Proof - t--85:

(p <=> p)	;
(p&p) / (pvp)	; t--60
p / p	; t--79, t--79

 Proof - t--86:

(pv~p)	;
(p&~p) + (p&~~p) + (~p&~p)	; t--44
(p&~p) + (p&p) + (~p&~p)	; t--31
0 + p + ~p	; a--24, t--79, t--79
1	; a--23

 Proof - t--87:

(p -> ~p)	;
(~pv~p)	; t--56
~p	; t--80

 Proof - t--88:

(p => ~p)	;
(p&~p) / p	; t--59
0 / p	; a--24

 Proof - t--89:

(p xor ~p)	;
(p&~~p) + (~p&~p)	; t--40
(p&p) + (~p&~p)	; t--31
p + ~p	; t--79, t--79
1	; a--23

 Proof - t--90:

(p <-> ~p)	;
(p&~p) + (~p&~~p)	; t--41
(p&~p) + (~p&p)	; t--31
(p&~p) + (p&~p)	; t--75
0 + 0	; a--24, a--24
0	; reduce

 Proof - t--91:

(p <=> ~p)	;
(p&~p) / (pv~p)	; t--60
0 / 1	; a--24, t--86
0	; reduce

 Proof - t--92:

(p&0)	;
(p&0) + p - p	; expand
(p&0) + (p&1) - p	; a--25
(p&0) + (p&~0) - p	; t--32
p - p	; t--35
0	; reduce

 Proof - t--93:

(pv0)	;
(p&0) + (p&~0) + (~p&0)	; t--44
0 + (p&1) + 0	; t--92, t--32, t--92
0 + p + 0	; a--25
p	; reduce

 Proof - t--94:

(p -> 0)	;
(~pv0)	; t--56
~p	; t--93

 Proof - t--95:

(p => 0)	;
(p&0) / p	; t--59
0 / p	; t--92

 Proof - t--96:

(p xor 0)	;
(p&~0) + (~p&0)	; t--40
(p&1) + (~p&0)	; t--32
p + 0	; a--25, t--92
p	; reduce

 Proof - t--97:

(p <-> 0)	;
(p&0) + (~p&~0)	; t--41
(p&0) + (~p&1)	; a--25
0 + ~p	; t--92
~p	; reduce

 Proof - t--98:

(p <=> 0)	;
(p&0) / (pv0)	; t--60
0 / p	; t--92, t--93

 Proof - t--99:

(pv1)	;
(p&1) + (p&~1) + (~p&1)	; t--44
(p&1) + (p&0) + (~p&1)	; t--33
p + 0 + ~p	; a--25, t--92, a--25
1	; a--23

 Proof - t--100:

(p -> 1)	;
(~pv1)	; t--56
1	; t--99

 Proof - t--101:

(p => 1)	;
(p&1) / p	; t--59
p / p	; a--25

 Proof - t--102:

(p xor 1)	;
(p&~1) + (~p&1)	; t--40
(p&0) + (~p&1)	; t--33
0 + ~p	; t--92, a--25
~p	; reduce

 Proof - t--103:

(p <-> 1)	;
(p&1) + (~p&~1)	; t--41
(p&1) + (~p&0)	; t--33
p + 0	; a--25, t--92
p	; reduce

 Proof - t--104:

(p <=> 1)	;
(p&1) / (pv1)	; t--60
p / 1	; a--25, t--99
p	; reduce

 Proof - t--105:

a	;
(p&q)	; d--6
pq + (ad-bc)	; t--73

 Proof - t--106:

b	;
(p&~q)	; d--7
p(~q) + A(p,~q)	; t--74
p(1-q) + A(p,~q)	; t--30
p - pq + A(p,~q)	; multiply
p - pq - (ad-bc)	; t--69

 Proof - t--107:

c	;
(~p&q)	; d--8
(~p)q + A(~p,q)	; t--74
(1-p)q + A(~p,q)	; t--30
q - pq + A(~p,q)	; multiply
q - pq - (ad-bc)	; t--70

 Proof - t--108:

d	;
(~p&~q)	; d--9
(~p)(~q) + A(~p,~q)	; t--74
(1-p)(1-q) + A(~p,~q)	; t--30, t--30
1 - p - q + pq + A(~p,~q)	; multiply
1 - p - q + pq + (ad-bc)	; t--71

 Proof - t--109:

(pvq)	;
p + q - (p&q)	; t--61
p + q - (pq + (ad-bc))	; t--73
p + q - pq - (ad-bc)	; rearrange

 Proof - t--110:

(p -> q)	;
a + c + d	; d--14
q + d	; t--37
q + 1 - p - q + pq + (ad-bc)	; t--108
1 - p + pq + (ad-bc)	; reduce

 Proof - t--111:

(p => q)	;
(p&q) / p	; t--59
(pq - (ad-bc)) / p	; t--73

 Proof - t--112:

(q -> p)	;
a + b + d	; t--54
p + d	; t--34
p + 1 - p - q + pq + (ad-bc)	; t--108
1 - q + pq + (ad-bc)	; reduce

 Proof - t--113:

(q => p)	;
(q&p) / q	; t--59
(p&q) / q	; t--75
(pq - (ad-bc)) / q	; t--73

 Proof - t--114:

(p xor q)	;
b + c	; d--11
(p&~q) + (~p&q)	; d--7, d--8
(p(~q)+A(p,~q)) + ((~p)q+A(~p,q))	; t--74, t--74
p(1-q) + A(p,~q) + (1-p)q + A(~p,q)	; t--30, t--30
p - pq + A(p,~q) + q - pq + A(~p,q)	; multiply
p - pq - (ad-bc) + q - pq - (ad-bc)	; t--69, t--70
p + q - 2pq - 2(ad-bc)	; rearrange

 Proof - t--115:

(p <-> q)	;
a + d	; d--12
a + d + b - b + c - c	; expand
(a+b+c+d) - (b+c)	; rearrange
1 - (p xor q)	; a--28, d--11
1 - (p + q - 2pq - 2(ad-bc))	; t--114
1 - p - q + 2pq +2(ad-bc)	; rearrange

 Proof - t--116:

(p <=> q)	;
(p&q) / (pvq)	; t--60
(pq - (ad-bc)) / (p + q - pq - (ad-bc))	; t--73, t--109

 Proof - t--117:

~(p&q)	;
~a	; d--6
1 - a	; t--30
(a+b+c+d) - a	; a--28
b + c + d	; reduce
(~pv~q)	; t--53

 Proof - t--118:

~(pvq)	;
1 - (pvq)	; t--30
(a+b+c+d) - (a+b+c)	; a--28, d--13
d	; reduce
(~p&~q)	; d--9

 Proof - t--119:

~(p -> q)	;
1 - (p -> q)	; t--30
(a+b+c+d) - (a+c+d)	; a--28, d--14
b	; reduce
(p&~q)	; d--7

 Proof - t--120:

~(p => q)	;
1 - (p => q)	; t--30
1 - a / (a+b)	; d--15
(a+b) / (a+b) - a / (a+b)	; expand
(a+b - a) / (a+b)	; rearrange
b / (a+b)	; reduce
(p&~q) / p	; d--7, t--34
(p => ~q)	; t--59

 Proof - t--121:

~(p xor q)	;
1 - (p xor q)	; t--30
(a+b+c+d) - (b+c)	; a--28, d--11
a + d	; reduce
(p <-> q)	; d--12

 Proof - t--122:

~(p <-> q)	;
1 - (p <-> q)	; t--30
(a+b+c+d) - (a+d)	; a--28, d--12
b + c	; reduce
(p xor q)	; d--11

 Proof - t--123:

~(p <=> q)	;
1 - (p <=> q)	; t--30
1 - a / (a+b+c)	; d--16
(a+b+c) / (a+b+c) - a / (a+b+c)	; expand
(a+b+c - a) / (a+b+c)	; rearrange
(b+c) / (a+b+c)	; reduce
(p xor q) / (pvq)	; d--11, d--13

 Proof - t--124:

(~p&(p -> q))	;
(~p&(~pvq))	; t--56
~p + (~pvq) - (~pv~pvq)	; t--68
~p + (~pvq) - (~pvq)	; t--79
~p	; reduce

 Proof - t--125:

(p&(p -> q))	;
(p&(~pvq))	; t--56
p + (~pvq) - (pv~pvq)	; t--68
p + (~pvq) - (1vq)	; t--86
p + (~pvq) - (qv1)	; t--75
p + (~pvq) - 1	; t--99
(a+b) + (a+c+d) - (a+b+c+d)	; t--34, t--52, a--28
a	; reduce

 No proof available - t:

 Proof - t--127:

p(p => q)	;
p((p&q) / p)	; t--59
(p&q)	; multiply

 Proof - t--128:

(~q&(p -> q))	;
(~q&(~pvq))	; t--56
~q + (~pvq) - (~qv~pvq)	; t--68
~q + (~pvq) - (~pv~qvq)	; t--75
~q + (~pvq) - (~pvqv~q)	; t--75
~q + (~pvq) - (~pv1)	; t--86
~q + (~pvq) - 1	; t--99
(b+d) + (a+c+d) - (a+b+c+d)	; t--50, t--52, a--28
d	; reduce
(~p&~q)	; d--9

 No proof available - t:

 Proof - t--130:

(~q -> ~p)	;
(~p&~q) + (~p&~~q) + (~~p&~~q)	; t--43
(~p&~q) + (~p&q) + (p&q)	; t--31, t--31
(p&q) + (~p&q) + (~p&~q)	; rearrange
(p -> q)	; t--42

 Proof - t--131:

(~q => ~p)	;
(~q&~p) / ~q	; t--59
(~p&~q) / ~q	; t--75
d / (b+d)	; d--9, t--50
a / (a+b)	; introduce
(p => q)	; d--15

 Definition - d--132:

e	;
("p, q and r are simultaneous satisfied")	;

 Definition - d--133:

f	;
("p, not-q and r are simultaneous satisfied")	;

 Definition - d--134:

g	;
("not-p, q and r are simultaneous satisfied")	;

 Definition - d--135:

h	;
("not-p, not-q and r are simultaneous satisfied")	;

 Definition - d--136:

i	;
("p, q and not-r are simultaneous satisfied")	;

 Definition - d--137:

j	;
("p, not-q and not-r are simultaneous satisfied")	;

 Definition - d--138:

k	;
("not-p, q and not-r are simultaneous satisfied")	;

 Definition - d--139:

l	;
("not-p, not-q and not-r are simultaneous satisfied")	;

 Definition - d--140:

a	;
e + i	;

 Definition - d--141:

b	;
f + j	;

 Definition - d--142:

c	;
g + k	;

 Definition - d--143:

d	;
h + l	;

 Definition - d--144:

(p&q&r)	;
e	;

 Definition - d--145:

(p&~q&r)	;
f	;

 Definition - d--146:

(~p&q&r)	;
g	;

 Definition - d--147:

(~p&~q&r)	;
h	;

 Definition - d--148:

(p&q&~r)	;
i	;

 Definition - d--149:

(p&~q&~r)	;
j	;

 Definition - d--150:

(~p&q&~r)	;
k	;

 Definition - d--151:

(~p&~q&~r)	;
l	;

 Proof - t--152:

(p&q)	;
a	; d--5
e + i	; d--140

 Proof - t--153:

(p&~q)	;
b	; d--6
f + j	; d--141

 Proof - t--154:

(~p&q)	;
c	; d--7
g + k	; d--142

 Proof - t--155:

(~p&~q)	;
d	; d--8
h + l	; d--143

 Proof - t--156:

(p&r)	;
(p&q&r) + (p&~q&r)	; t--35
e + f	; d--144, d--145

 Proof - t--157:

(p&~r)	;
(p&q&~r) + (p&~q&~r)	; t--35
i + j	; d--148, d--149

 Proof - t--158:

(~p&r)	;
(~p&q&r) + (~p&~q&r)	; t--35
g + h	; d--146, d--147

 Proof - t--159:

(~p&~r)	;
(~p&q&~r) + (~p&~q&~r)	; t--35
k+ l	; d--150, d--151

 Proof - t--160:

(q&r)	;
(p&q&r) + (~p&q&r)	; t--36
e + g	; d--144, d--146

 Proof - t--161:

(q&~r)	;
(p&q&~r) + (~p&q&~r)	; t--36
i + k	; d--148, d--150

 Proof - t--162:

(~q&r)	;
(p&~q&r) + (~p&~q&r)	; t--36
f + h	; d--145, d--147

 Proof - t--163:

(~q&~r)	;
(p&~q&~r) + (~p&~q&~r)	; t--36
j + l	; d--149, d--151

 Proof - t--164:

;

;

;

 Proof - t--165:

;

;

;

 Proof - t--166:

;

;

;

 Proof - t--167:

;

;

;

 Proof - t--168:

;

;

;

 Proof - t--169:

;

;

;

 Proof - t--170:

((p&q)&r)	;
(p&q) + r - ((p&q)vr)	;
(p&q) + r - ((p&q)vr)	;

 Proof - t--171:

;

;

;

;

 Proof - t--172:

((pvq)vr)	;
(~(~p&~q)vr)	;
~((~p&~q)&~r)	;
~(~p&(~q&~r))	;
(pv~(~q&~r))	;
(pv(qvr))	;

 Proof - t--173:

((pvq)&(pvr))	;
(pvq) + (pvr) - ((pvq)v(pvr))	;
(pvq) + (pvr) - (pvqvr)	;
~(~p&~q) + ~(~p&~r) - ~(~p&~q&~r)	;
1 - (~p&~q) + 1 - (~p&~r) - 1 - (~p&~q&~r)	;
1 - (h+l) + 1 - (k+l) - 1 - l	;
1 - (h+k+l)	;
(e+f+g+h+i+j+k+l) - (h+k+l)	;
e + f + g + i + j	;
(e+i+f+j) + (e+g) - e	;
(a+b) + (e+g) - e	;
p + (q&r) - (p&q&r)	;
p + (q&r) - (p&(q&r))	;
(pv(q&r))	;

 Proof - t--174:

(p&(qvr))	;
~~(p&~~(qvr))	;
~(~pv(~q&~r))	;
~((~pv~q)&(~pv~r))	;
~(~~(~pv~q)&~~(~pv~r))	;
~(~(p&q)&~(p&r))	;
((p&q)v(p&r))	;

 No proof available - t:

;

;

;

;

;

;

;

;

;

;

;