:: GATE_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: GATE_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, p being set st $ g0 & $ g12 & ( $ b0 implies $ XOR2 p,(AND2 g0,a11) ) & ( $ XOR2 p,(AND2 g0,a11) implies $ b0 ) & ( $ b1 implies $ XOR2 a0,(AND2 g1,a11) ) & ( $ XOR2 a0,(AND2 g1,a11) implies $ b1 ) & ( $ b2 implies $ XOR2 a1,(AND2 g2,a11) ) & ( $ XOR2 a1,(AND2 g2,a11) implies $ b2 ) & ( $ b3 implies $ XOR2 a2,(AND2 g3,a11) ) & ( $ XOR2 a2,(AND2 g3,a11) implies $ b3 ) & ( $ b4 implies $ XOR2 a3,(AND2 g4,a11) ) & ( $ XOR2 a3,(AND2 g4,a11) implies $ b4 ) & ( $ b5 implies $ XOR2 a4,(AND2 g5,a11) ) & ( $ XOR2 a4,(AND2 g5,a11) implies $ b5 ) & ( $ b6 implies $ XOR2 a5,(AND2 g6,a11) ) & ( $ XOR2 a5,(AND2 g6,a11) implies $ b6 ) & ( $ b7 implies $ XOR2 a6,(AND2 g7,a11) ) & ( $ XOR2 a6,(AND2 g7,a11) implies $ b7 ) & ( $ b8 implies $ XOR2 a7,(AND2 g8,a11) ) & ( $ XOR2 a7,(AND2 g8,a11) implies $ b8 ) & ( $ b9 implies $ XOR2 a8,(AND2 g9,a11) ) & ( $ XOR2 a8,(AND2 g9,a11) implies $ b9 ) & ( $ b10 implies $ XOR2 a9,(AND2 g10,a11) ) & ( $ XOR2 a9,(AND2 g10,a11) implies $ b10 ) & ( $ b11 implies $ XOR2 a10,(AND2 g11,a11) ) & ( $ XOR2 a10,(AND2 g11,a11) implies $ b11 ) holds
( ( $ a11 implies $ AND2 g12,a11 ) & ( $ AND2 g12,a11 implies $ a11 ) & ( $ a10 implies $ XOR2 b11,(AND2 g11,a11) ) & ( $ XOR2 b11,(AND2 g11,a11) implies $ a10 ) & ( $ a9 implies $ XOR2 b10,(AND2 g10,a11) ) & ( $ XOR2 b10,(AND2 g10,a11) implies $ a9 ) & ( $ a8 implies $ XOR2 b9,(AND2 g9,a11) ) & ( $ XOR2 b9,(AND2 g9,a11) implies $ a8 ) & ( $ a7 implies $ XOR2 b8,(AND2 g8,a11) ) & ( $ XOR2 b8,(AND2 g8,a11) implies $ a7 ) & ( $ a6 implies $ XOR2 b7,(AND2 g7,a11) ) & ( $ XOR2 b7,(AND2 g7,a11) implies $ a6 ) & ( $ a5 implies $ XOR2 b6,(AND2 g6,a11) ) & ( $ XOR2 b6,(AND2 g6,a11) implies $ a5 ) & ( $ a4 implies $ XOR2 b5,(AND2 g5,a11) ) & ( $ XOR2 b5,(AND2 g5,a11) implies $ a4 ) & ( $ a3 implies $ XOR2 b4,(AND2 g4,a11) ) & ( $ XOR2 b4,(AND2 g4,a11) implies $ a3 ) & ( $ a2 implies $ XOR2 b3,(AND2 g3,a11) ) & ( $ XOR2 b3,(AND2 g3,a11) implies $ a2 ) & ( $ a1 implies $ XOR2 b2,(AND2 g2,a11) ) & ( $ XOR2 b2,(AND2 g2,a11) implies $ a1 ) & ( $ a0 implies $ XOR2 b1,(AND2 g1,a11) ) & ( $ XOR2 b1,(AND2 g1,a11) implies $ a0 ) & ( $ p implies $ XOR2 b0,(AND2 g0,a11) ) & ( $ XOR2 b0,(AND2 g0,a11) implies $ p ) )
proof end;

theorem :: GATE_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, p being set st $ g0 & $ g16 & ( $ b0 implies $ XOR2 p,(AND2 g0,a15) ) & ( $ XOR2 p,(AND2 g0,a15) implies $ b0 ) & ( $ b1 implies $ XOR2 a0,(AND2 g1,a15) ) & ( $ XOR2 a0,(AND2 g1,a15) implies $ b1 ) & ( $ b2 implies $ XOR2 a1,(AND2 g2,a15) ) & ( $ XOR2 a1,(AND2 g2,a15) implies $ b2 ) & ( $ b3 implies $ XOR2 a2,(AND2 g3,a15) ) & ( $ XOR2 a2,(AND2 g3,a15) implies $ b3 ) & ( $ b4 implies $ XOR2 a3,(AND2 g4,a15) ) & ( $ XOR2 a3,(AND2 g4,a15) implies $ b4 ) & ( $ b5 implies $ XOR2 a4,(AND2 g5,a15) ) & ( $ XOR2 a4,(AND2 g5,a15) implies $ b5 ) & ( $ b6 implies $ XOR2 a5,(AND2 g6,a15) ) & ( $ XOR2 a5,(AND2 g6,a15) implies $ b6 ) & ( $ b7 implies $ XOR2 a6,(AND2 g7,a15) ) & ( $ XOR2 a6,(AND2 g7,a15) implies $ b7 ) & ( $ b8 implies $ XOR2 a7,(AND2 g8,a15) ) & ( $ XOR2 a7,(AND2 g8,a15) implies $ b8 ) & ( $ b9 implies $ XOR2 a8,(AND2 g9,a15) ) & ( $ XOR2 a8,(AND2 g9,a15) implies $ b9 ) & ( $ b10 implies $ XOR2 a9,(AND2 g10,a15) ) & ( $ XOR2 a9,(AND2 g10,a15) implies $ b10 ) & ( $ b11 implies $ XOR2 a10,(AND2 g11,a15) ) & ( $ XOR2 a10,(AND2 g11,a15) implies $ b11 ) & ( $ b12 implies $ XOR2 a11,(AND2 g12,a15) ) & ( $ XOR2 a11,(AND2 g12,a15) implies $ b12 ) & ( $ b13 implies $ XOR2 a12,(AND2 g13,a15) ) & ( $ XOR2 a12,(AND2 g13,a15) implies $ b13 ) & ( $ b14 implies $ XOR2 a13,(AND2 g14,a15) ) & ( $ XOR2 a13,(AND2 g14,a15) implies $ b14 ) & ( $ b15 implies $ XOR2 a14,(AND2 g15,a15) ) & ( $ XOR2 a14,(AND2 g15,a15) implies $ b15 ) holds
( ( $ a15 implies $ AND2 g16,a15 ) & ( $ AND2 g16,a15 implies $ a15 ) & ( $ a14 implies $ XOR2 b15,(AND2 g15,a15) ) & ( $ XOR2 b15,(AND2 g15,a15) implies $ a14 ) & ( $ a13 implies $ XOR2 b14,(AND2 g14,a15) ) & ( $ XOR2 b14,(AND2 g14,a15) implies $ a13 ) & ( $ a12 implies $ XOR2 b13,(AND2 g13,a15) ) & ( $ XOR2 b13,(AND2 g13,a15) implies $ a12 ) & ( $ a11 implies $ XOR2 b12,(AND2 g12,a15) ) & ( $ XOR2 b12,(AND2 g12,a15) implies $ a11 ) & ( $ a10 implies $ XOR2 b11,(AND2 g11,a15) ) & ( $ XOR2 b11,(AND2 g11,a15) implies $ a10 ) & ( $ a9 implies $ XOR2 b10,(AND2 g10,a15) ) & ( $ XOR2 b10,(AND2 g10,a15) implies $ a9 ) & ( $ a8 implies $ XOR2 b9,(AND2 g9,a15) ) & ( $ XOR2 b9,(AND2 g9,a15) implies $ a8 ) & ( $ a7 implies $ XOR2 b8,(AND2 g8,a15) ) & ( $ XOR2 b8,(AND2 g8,a15) implies $ a7 ) & ( $ a6 implies $ XOR2 b7,(AND2 g7,a15) ) & ( $ XOR2 b7,(AND2 g7,a15) implies $ a6 ) & ( $ a5 implies $ XOR2 b6,(AND2 g6,a15) ) & ( $ XOR2 b6,(AND2 g6,a15) implies $ a5 ) & ( $ a4 implies $ XOR2 b5,(AND2 g5,a15) ) & ( $ XOR2 b5,(AND2 g5,a15) implies $ a4 ) & ( $ a3 implies $ XOR2 b4,(AND2 g4,a15) ) & ( $ XOR2 b4,(AND2 g4,a15) implies $ a3 ) & ( $ a2 implies $ XOR2 b3,(AND2 g3,a15) ) & ( $ XOR2 b3,(AND2 g3,a15) implies $ a2 ) & ( $ a1 implies $ XOR2 b2,(AND2 g2,a15) ) & ( $ XOR2 b2,(AND2 g2,a15) implies $ a1 ) & ( $ a0 implies $ XOR2 b1,(AND2 g1,a15) ) & ( $ XOR2 b1,(AND2 g1,a15) implies $ a0 ) & ( $ p implies $ XOR2 b0,(AND2 g0,a15) ) & ( $ XOR2 b0,(AND2 g0,a15) implies $ p ) )
proof end;

theorem :: GATE_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, z, p being set st $ g0 & $ g12 & not $ z & ( $ b0 implies $ XOR2 p,a11 ) & ( $ XOR2 p,a11 implies $ b0 ) & ( $ b1 implies $ XOR2 a0,(AND2 g1,b0) ) & ( $ XOR2 a0,(AND2 g1,b0) implies $ b1 ) & ( $ b2 implies $ XOR2 a1,(AND2 g2,b0) ) & ( $ XOR2 a1,(AND2 g2,b0) implies $ b2 ) & ( $ b3 implies $ XOR2 a2,(AND2 g3,b0) ) & ( $ XOR2 a2,(AND2 g3,b0) implies $ b3 ) & ( $ b4 implies $ XOR2 a3,(AND2 g4,b0) ) & ( $ XOR2 a3,(AND2 g4,b0) implies $ b4 ) & ( $ b5 implies $ XOR2 a4,(AND2 g5,b0) ) & ( $ XOR2 a4,(AND2 g5,b0) implies $ b5 ) & ( $ b6 implies $ XOR2 a5,(AND2 g6,b0) ) & ( $ XOR2 a5,(AND2 g6,b0) implies $ b6 ) & ( $ b7 implies $ XOR2 a6,(AND2 g7,b0) ) & ( $ XOR2 a6,(AND2 g7,b0) implies $ b7 ) & ( $ b8 implies $ XOR2 a7,(AND2 g8,b0) ) & ( $ XOR2 a7,(AND2 g8,b0) implies $ b8 ) & ( $ b9 implies $ XOR2 a8,(AND2 g9,b0) ) & ( $ XOR2 a8,(AND2 g9,b0) implies $ b9 ) & ( $ b10 implies $ XOR2 a9,(AND2 g10,b0) ) & ( $ XOR2 a9,(AND2 g10,b0) implies $ b10 ) & ( $ b11 implies $ XOR2 a10,(AND2 g11,b0) ) & ( $ XOR2 a10,(AND2 g11,b0) implies $ b11 ) holds
( ( $ b11 implies $ XOR2 (XOR2 a10,(AND2 g11,a11)),(XOR2 z,(AND2 g11,p)) ) & ( $ XOR2 (XOR2 a10,(AND2 g11,a11)),(XOR2 z,(AND2 g11,p)) implies $ b11 ) & ( $ b10 implies $ XOR2 (XOR2 a9,(AND2 g10,a11)),(XOR2 z,(AND2 g10,p)) ) & ( $ XOR2 (XOR2 a9,(AND2 g10,a11)),(XOR2 z,(AND2 g10,p)) implies $ b10 ) & ( $ b9 implies $ XOR2 (XOR2 a8,(AND2 g9,a11)),(XOR2 z,(AND2 g9,p)) ) & ( $ XOR2 (XOR2 a8,(AND2 g9,a11)),(XOR2 z,(AND2 g9,p)) implies $ b9 ) & ( $ b8 implies $ XOR2 (XOR2 a7,(AND2 g8,a11)),(XOR2 z,(AND2 g8,p)) ) & ( $ XOR2 (XOR2 a7,(AND2 g8,a11)),(XOR2 z,(AND2 g8,p)) implies $ b8 ) & ( $ b7 implies $ XOR2 (XOR2 a6,(AND2 g7,a11)),(XOR2 z,(AND2 g7,p)) ) & ( $ XOR2 (XOR2 a6,(AND2 g7,a11)),(XOR2 z,(AND2 g7,p)) implies $ b7 ) & ( $ b6 implies $ XOR2 (XOR2 a5,(AND2 g6,a11)),(XOR2 z,(AND2 g6,p)) ) & ( $ XOR2 (XOR2 a5,(AND2 g6,a11)),(XOR2 z,(AND2 g6,p)) implies $ b6 ) & ( $ b5 implies $ XOR2 (XOR2 a4,(AND2 g5,a11)),(XOR2 z,(AND2 g5,p)) ) & ( $ XOR2 (XOR2 a4,(AND2 g5,a11)),(XOR2 z,(AND2 g5,p)) implies $ b5 ) & ( $ b4 implies $ XOR2 (XOR2 a3,(AND2 g4,a11)),(XOR2 z,(AND2 g4,p)) ) & ( $ XOR2 (XOR2 a3,(AND2 g4,a11)),(XOR2 z,(AND2 g4,p)) implies $ b4 ) & ( $ b3 implies $ XOR2 (XOR2 a2,(AND2 g3,a11)),(XOR2 z,(AND2 g3,p)) ) & ( $ XOR2 (XOR2 a2,(AND2 g3,a11)),(XOR2 z,(AND2 g3,p)) implies $ b3 ) & ( $ b2 implies $ XOR2 (XOR2 a1,(AND2 g2,a11)),(XOR2 z,(AND2 g2,p)) ) & ( $ XOR2 (XOR2 a1,(AND2 g2,a11)),(XOR2 z,(AND2 g2,p)) implies $ b2 ) & ( $ b1 implies $ XOR2 (XOR2 a0,(AND2 g1,a11)),(XOR2 z,(AND2 g1,p)) ) & ( $ XOR2 (XOR2 a0,(AND2 g1,a11)),(XOR2 z,(AND2 g1,p)) implies $ b1 ) & ( $ b0 implies $ XOR2 (XOR2 z,(AND2 g0,a11)),(XOR2 z,(AND2 g0,p)) ) & ( $ XOR2 (XOR2 z,(AND2 g0,a11)),(XOR2 z,(AND2 g0,p)) implies $ b0 ) )
proof end;

theorem :: GATE_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, z, p being set st $ g0 & $ g16 & not $ z & ( $ b0 implies $ XOR2 p,a15 ) & ( $ XOR2 p,a15 implies $ b0 ) & ( $ b1 implies $ XOR2 a0,(AND2 g1,b0) ) & ( $ XOR2 a0,(AND2 g1,b0) implies $ b1 ) & ( $ b2 implies $ XOR2 a1,(AND2 g2,b0) ) & ( $ XOR2 a1,(AND2 g2,b0) implies $ b2 ) & ( $ b3 implies $ XOR2 a2,(AND2 g3,b0) ) & ( $ XOR2 a2,(AND2 g3,b0) implies $ b3 ) & ( $ b4 implies $ XOR2 a3,(AND2 g4,b0) ) & ( $ XOR2 a3,(AND2 g4,b0) implies $ b4 ) & ( $ b5 implies $ XOR2 a4,(AND2 g5,b0) ) & ( $ XOR2 a4,(AND2 g5,b0) implies $ b5 ) & ( $ b6 implies $ XOR2 a5,(AND2 g6,b0) ) & ( $ XOR2 a5,(AND2 g6,b0) implies $ b6 ) & ( $ b7 implies $ XOR2 a6,(AND2 g7,b0) ) & ( $ XOR2 a6,(AND2 g7,b0) implies $ b7 ) & ( $ b8 implies $ XOR2 a7,(AND2 g8,b0) ) & ( $ XOR2 a7,(AND2 g8,b0) implies $ b8 ) & ( $ b9 implies $ XOR2 a8,(AND2 g9,b0) ) & ( $ XOR2 a8,(AND2 g9,b0) implies $ b9 ) & ( $ b10 implies $ XOR2 a9,(AND2 g10,b0) ) & ( $ XOR2 a9,(AND2 g10,b0) implies $ b10 ) & ( $ b11 implies $ XOR2 a10,(AND2 g11,b0) ) & ( $ XOR2 a10,(AND2 g11,b0) implies $ b11 ) & ( $ b12 implies $ XOR2 a11,(AND2 g12,b0) ) & ( $ XOR2 a11,(AND2 g12,b0) implies $ b12 ) & ( $ b13 implies $ XOR2 a12,(AND2 g13,b0) ) & ( $ XOR2 a12,(AND2 g13,b0) implies $ b13 ) & ( $ b14 implies $ XOR2 a13,(AND2 g14,b0) ) & ( $ XOR2 a13,(AND2 g14,b0) implies $ b14 ) & ( $ b15 implies $ XOR2 a14,(AND2 g15,b0) ) & ( $ XOR2 a14,(AND2 g15,b0) implies $ b15 ) holds
( ( $ b15 implies $ XOR2 (XOR2 a14,(AND2 g15,a15)),(XOR2 z,(AND2 g15,p)) ) & ( $ XOR2 (XOR2 a14,(AND2 g15,a15)),(XOR2 z,(AND2 g15,p)) implies $ b15 ) & ( $ b14 implies $ XOR2 (XOR2 a13,(AND2 g14,a15)),(XOR2 z,(AND2 g14,p)) ) & ( $ XOR2 (XOR2 a13,(AND2 g14,a15)),(XOR2 z,(AND2 g14,p)) implies $ b14 ) & ( $ b13 implies $ XOR2 (XOR2 a12,(AND2 g13,a15)),(XOR2 z,(AND2 g13,p)) ) & ( $ XOR2 (XOR2 a12,(AND2 g13,a15)),(XOR2 z,(AND2 g13,p)) implies $ b13 ) & ( $ b12 implies $ XOR2 (XOR2 a11,(AND2 g12,a15)),(XOR2 z,(AND2 g12,p)) ) & ( $ XOR2 (XOR2 a11,(AND2 g12,a15)),(XOR2 z,(AND2 g12,p)) implies $ b12 ) & ( $ b11 implies $ XOR2 (XOR2 a10,(AND2 g11,a15)),(XOR2 z,(AND2 g11,p)) ) & ( $ XOR2 (XOR2 a10,(AND2 g11,a15)),(XOR2 z,(AND2 g11,p)) implies $ b11 ) & ( $ b10 implies $ XOR2 (XOR2 a9,(AND2 g10,a15)),(XOR2 z,(AND2 g10,p)) ) & ( $ XOR2 (XOR2 a9,(AND2 g10,a15)),(XOR2 z,(AND2 g10,p)) implies $ b10 ) & ( $ b9 implies $ XOR2 (XOR2 a8,(AND2 g9,a15)),(XOR2 z,(AND2 g9,p)) ) & ( $ XOR2 (XOR2 a8,(AND2 g9,a15)),(XOR2 z,(AND2 g9,p)) implies $ b9 ) & ( $ b8 implies $ XOR2 (XOR2 a7,(AND2 g8,a15)),(XOR2 z,(AND2 g8,p)) ) & ( $ XOR2 (XOR2 a7,(AND2 g8,a15)),(XOR2 z,(AND2 g8,p)) implies $ b8 ) & ( $ b7 implies $ XOR2 (XOR2 a6,(AND2 g7,a15)),(XOR2 z,(AND2 g7,p)) ) & ( $ XOR2 (XOR2 a6,(AND2 g7,a15)),(XOR2 z,(AND2 g7,p)) implies $ b7 ) & ( $ b6 implies $ XOR2 (XOR2 a5,(AND2 g6,a15)),(XOR2 z,(AND2 g6,p)) ) & ( $ XOR2 (XOR2 a5,(AND2 g6,a15)),(XOR2 z,(AND2 g6,p)) implies $ b6 ) & ( $ b5 implies $ XOR2 (XOR2 a4,(AND2 g5,a15)),(XOR2 z,(AND2 g5,p)) ) & ( $ XOR2 (XOR2 a4,(AND2 g5,a15)),(XOR2 z,(AND2 g5,p)) implies $ b5 ) & ( $ b4 implies $ XOR2 (XOR2 a3,(AND2 g4,a15)),(XOR2 z,(AND2 g4,p)) ) & ( $ XOR2 (XOR2 a3,(AND2 g4,a15)),(XOR2 z,(AND2 g4,p)) implies $ b4 ) & ( $ b3 implies $ XOR2 (XOR2 a2,(AND2 g3,a15)),(XOR2 z,(AND2 g3,p)) ) & ( $ XOR2 (XOR2 a2,(AND2 g3,a15)),(XOR2 z,(AND2 g3,p)) implies $ b3 ) & ( $ b2 implies $ XOR2 (XOR2 a1,(AND2 g2,a15)),(XOR2 z,(AND2 g2,p)) ) & ( $ XOR2 (XOR2 a1,(AND2 g2,a15)),(XOR2 z,(AND2 g2,p)) implies $ b2 ) & ( $ b1 implies $ XOR2 (XOR2 a0,(AND2 g1,a15)),(XOR2 z,(AND2 g1,p)) ) & ( $ XOR2 (XOR2 a0,(AND2 g1,a15)),(XOR2 z,(AND2 g1,p)) implies $ b1 ) & ( $ b0 implies $ XOR2 (XOR2 z,(AND2 g0,a15)),(XOR2 z,(AND2 g0,p)) ) & ( $ XOR2 (XOR2 z,(AND2 g0,a15)),(XOR2 z,(AND2 g0,p)) implies $ b0 ) )
proof end;