prove ((A1 & A2) => (A2 & A1)). prove ((((A1 => A2) & (A2 => A1)) => (A1 & A2)) & (((A2 => A1) & (A1 => A2)) => (A1 & A2))) => (A0 v (A1 & A2) v ~A0). % prove ((((A1 => A2) & (A2 => A1)) => (A1 & A2 & A3)) & (((A2 => A3) & (A3 => A2)) => (A1 & A2 & A3)) & (((A3 => A1) & (A1 => A3)) => (A1 & A2 & A3))) => (A1 & A2 & A3). prove (P11 & P21) => P11 & P21. prove (~~P11 & ~~P21) => P11 & P21. prove ((A1 v (A1 => C)) => C) => C. refute ((A1 v ~~A1 => C) => C) => C. prove (((A0 => C) & (B1 => B0) => A1) & ((B0 => A1) => A0) => C) & (((B0 => A1) => A0) & ((B1 => B0) => A1) & (A0 => C) => C). prove A1 & (A1 => A1 => A0) => A0. refute ~A1 & (A1 => A1 => A0) => A0. prove (P11 & P21) => P11 & P21. prove (~~P11 & ~~P21) => P11 & P21. prove ((A1 v (A1 => C)) => C) => C. refute ((A1 v ~~A1 => C) => C) => C. refute ~A1 & (A1 => A1 => A0) => A0. prove A1 & (A1 => A1 => A0) => A0. prove ((((A1 => A2) & (A2 => A1)) => (A1 & A2)) & (((A2 => A1) & (A1 => A2)) => (A1 & A2))) => (A0 v (A1 & A2) v ~A0). prove (((A0 => C) & (B1 => B0) => A1) & ((B0 => A1) => A0) => C) & (((B0 => A1) => A0) & ((B1 => B0) => A1) & (A0 => C) => C). % 40 of Chad's examples generated by a LISP program which makes % random (intuitionistic) tautologies. % success: % prove (((B => B) => (D & A)) => (((C v C) & A & (~A => (A & D)) & ~(B & D)) => (((C v C) & D) => ((~D v ~A v (B => B) v ((B => B) => (D & A))) & (~(B & B) v ((~B => ~B) & (C v C))))))). % prove (((D => (C => A)) & A & ((C & A) => (C & B)) & ((A v (C => A)) => (A & D & ~(C v A)))) => (D => ~(C v A))). % prove ~(~~~(A => A) & (((D & B & (B => B)) => ~(A => B)) => B)). % prove (((C => A) => (C v D)) => (((C v D) => ~A) => (((C => A) & (~A => (C v A)) & ~~(D v C) & (D v B)) => (A => (C v A))))). % prove ((((C => D) => (A & (B => B))) & D & (C => D) & C & ((B => A) v (C & B))) => (((((C => C) & (B => B)) => (B v C)) & D) => (((A & D) v A) => ((C & (B => B) & (C => C) & C) => ~~(B v C))))). %% too hard % prove ~((((B v C) & ((D => B) v A) & D) => ((D v A) & (B => D))) & ((D v D) => (D & D)) & (D => B) & (D v A) & (A => B) & ((D v B) => (D & A & A)) & (A v B v (B & B)) & ((B => D) => C) & ((D v A) => (D v D)) & ~C & ((A & A) => (A & B & (B v C) & C)) & (D v B)). prove (D => (~((A => B) v C) => ~(A => B))). prove ((~((D => C) v C v (A & C & (C => B))) & ((D & D) v ((D & (C => A)) => ~(C v A)) v ((B & ~B) => ((C & C) v (D => B))))) => (((D & D) => C) => (((D & (C => A)) => ~(C v A)) v ((B & ~B) => ((C & C) v (D => B)))))). prove ((((C & (D => D)) => C) & (C => D) & (C => B) & C & D & C) => (((B => A) & D) => ((A v C) => ((D => D) => ((B => A) & (A v C v C) & ((B & C) => (B & C)) & (A v C)))))). prove (((C => C) => (B & A)) => ((C & D) => ((C => C) => ((C & A & D) => ((A v A) => (~(C => (B & A & ~A)) v ((A v A) & B & A & C & D & (((B => B) => D) => (A & D))))))))). prove (((((A & A) => ((A & A) v C)) => B) & ((~(A v D) => ((C => B) & (A => A))) => (D & ((C => B) => A))) & ~(D => D)) => (B v ~A)). prove ~((((D & A) => (A => C)) v (D & C) v (D => B)) & ~A & ~(((D & A) => (A => C)) v (D & C) v (D => B))). prove (((A v C) & (~C => (B & C)) & ((B & C) => (D => D)) & ((D v ((D & A) => ~A)) => D) & (B => C) & A) => (~C => ((B => C) v C v C v C v C v C))). prove ((((~(C & A) => ((D v B) & (B => B))) v ~(B => (A => B))) & (A => B) & (B => D) & ((A => B) v (B & A)) & (C v C) & (A v D) & A & ((A & C) => (C & B))) => ((A v D) & (A v C v ((B => D) & (A => B))))). prove ~(~(D & B & (D v C)) & ~(B v ~(D v C)) & D & B). prove ((D & B & (C v A)) => ((((~B v (D & C)) => (((C v A) => B) & B)) & (B => ~(C & D))) => (((D => (D & C & D)) & (B => A)) => ~(C & D)))). % The next one is challenging. - Chad % The Goddess proves it in about 8 minutes. prove ((((C v A) => (C v A)) => (~A & B)) => ((~(((D v D) => (B & D)) v ~A) v ((B v C) => (B & A & A))) => ((B & ((D & D) => (A & C)) & (B v C)) => ((((C & D) => (D => B)) => ~B) v (A & A))))). prove (~(((D v B) & (B v D)) v ((A v C) => (C => C))) => (~B v ~(((D v B) & (B v D)) v ((A v C) => (C => C))))). prove ((((A v (A & A)) => ((B => D) => C)) & B & ~~~D) => ((A v ((A v (A & A)) => ((B => D) => C))) & B & ~~~D)). prove (((C & C & (D v B)) v ~A) => (((C v A) => (C v D)) => (((B => D) & C & B & C & ~(~D & ~D & (C v C v (B & D))) & ~((B => D) & ~A) & ~(C v C)) => ((C v A) => ((C v D) & C & B))))). prove (B => ((~D & ~A) => ((C & C & A) => (((C v C) & (((((B v C) & (C v C)) v A v C v (A & C)) => ~(~D v D)) v ((C & D) => ((B v A) & A)))) => ((D & C & D) => ((B v A) & (B v (C & A)))))))). prove ((B => (~A v ~D)) => ~~(B => (~A v ~D))). prove ~(C & ~A & ((D & C) v (D & A) v (B => (B v C)) v (A => ((B & C) v D v C))) & ((~C => (~C & C & C)) => ~((C & C) => C)) & (~B => (C & C)) & (~A => ~B)). prove ((((B => D) => (B & D)) => ~B) => ((A & (D v B) & ~A) v ~(~A => (D => C)) v (((B => D) => (B & D)) => (B => ~B)))). prove ((~A v ~D v ~((B => D) & (D v B))) => (~A v ~D v ~((B => D) & (D v B)))). prove ~((~B => (B => A)) & ~(B => B) & (((~B => (B => A)) & ((C & D) v (A & D))) => ((B v A) & ~D)) & B & A & ((C v A) => ((C v B) => (C & D))) & (C v B) & ((D & A) v B v ~(B v A)) & D & ~(C v A)). prove ((((C => (D & C)) & ~(D & D)) => (C => (D & C))) v ~(((D v C) & D & D) v B v D v ~A)). prove ((B & (B => A) & A & B) => (A & ((C & (C v C) & C) => (B v C v C)))). prove ((((~C & (C v (B => C))) => ~((C & A) => (C & A))) & (B => C)) => (~(~C & B) v (~(B v B) => A) v A)). prove ~(((A & D) => ~A) & C & D & A & D & (D => D) & (D v B) & ((~B & (D => A)) => ~D) & ((~(C => B) v ((C => C) & ((C v A) => (C v A)))) => (A & (C v A))) & (((B v D v B) & ~A) => ~(A v C v A))). prove ((~(D & D) & ((~(A => B) => ~(B => B)) => ~C) & ~(D v C) & (~(B & D) v (D & D))) => ~(B & D)). prove (((~(((D => D) => (D => D)) v D v A) v (~C => ~D)) & A) => ((C & ~A & (((D => A) & C & D) v ((~C => ~D) => ~~A))) => ((D & D) v A v ((D => D) & C & B) v ((D => D) & (D => A))))). prove (((~D => (B => A)) & (~B => (C v B)) & ~B & (D v C v (A => B)) & D & (((D => C) & D) v C)) => ((~D => (B => A)) & (~B => (C v B)) & ~B & (((D => C) & D) v C))). prove ~(((~(C & C) => ~(C & C)) & (D v B v ~D v ((D => B) => (D => B)) v (B & C))) => ~((C & A) v ((B => C) => (B => C)) v B v (B & D))). prove (((~C v (((A v D) => (C & D)) => ((A v D) => (C & D)))) => (A & (((B v C) & A) => ((D => C) v B)))) => ~((B => B) => ~A)). prove ~(~((A => A) => (A & D & D & (~C v (B & C)))) & A & D & D & ((A => A) => (B & C))). prove ~((~((D & B) => ~B) v A) & (C v B) & D & (D => B) & C & ~(C v B)). prove ((~(~A & (D v C)) v ~~D) => ((((A v (B => B) v B) => (A v (B => B))) & D & (B => B)) => (A v (B => B)))). prove ~(~(((D v B) & B) => (D v B)) & ~~(B v A)). prove (((~B => D) & D & (C => C)) => ((D & A & (~(D & A) => (~C v (D => A)))) => ((D & A & (~B => D)) v ((~(B & A) => D) => ~(A & A & (C => A)))))).