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

theorem :: GATE_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3 being set holds
not ( ( $ s0 implies $ AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) ) & ( $ AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) implies $ s0 ) & ( $ s1 implies $ AND3 (NOT1 q3),(NOT1 q2),q1 ) & ( $ AND3 (NOT1 q3),(NOT1 q2),q1 implies $ s1 ) & ( $ s2 implies $ AND3 (NOT1 q3),q2,(NOT1 q1) ) & ( $ AND3 (NOT1 q3),q2,(NOT1 q1) implies $ s2 ) & ( $ s3 implies $ AND3 (NOT1 q3),q2,q1 ) & ( $ AND3 (NOT1 q3),q2,q1 implies $ s3 ) & ( $ s4 implies $ AND3 q3,(NOT1 q2),(NOT1 q1) ) & ( $ AND3 q3,(NOT1 q2),(NOT1 q1) implies $ s4 ) & ( $ s5 implies $ AND3 q3,(NOT1 q2),q1 ) & ( $ AND3 q3,(NOT1 q2),q1 implies $ s5 ) & ( $ s6 implies $ AND3 q3,q2,(NOT1 q1) ) & ( $ AND3 q3,q2,(NOT1 q1) implies $ s6 ) & ( $ s7 implies $ AND3 q3,q2,q1 ) & ( $ AND3 q3,q2,q1 implies $ s7 ) & ( $ ns0 implies $ AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) ) & ( $ AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) implies $ ns0 ) & ( $ ns1 implies $ AND3 (NOT1 nq3),(NOT1 nq2),nq1 ) & ( $ AND3 (NOT1 nq3),(NOT1 nq2),nq1 implies $ ns1 ) & ( $ ns2 implies $ AND3 (NOT1 nq3),nq2,(NOT1 nq1) ) & ( $ AND3 (NOT1 nq3),nq2,(NOT1 nq1) implies $ ns2 ) & ( $ ns3 implies $ AND3 (NOT1 nq3),nq2,nq1 ) & ( $ AND3 (NOT1 nq3),nq2,nq1 implies $ ns3 ) & ( $ ns4 implies $ AND3 nq3,(NOT1 nq2),(NOT1 nq1) ) & ( $ AND3 nq3,(NOT1 nq2),(NOT1 nq1) implies $ ns4 ) & ( $ ns5 implies $ AND3 nq3,(NOT1 nq2),nq1 ) & ( $ AND3 nq3,(NOT1 nq2),nq1 implies $ ns5 ) & ( $ ns6 implies $ AND3 nq3,nq2,(NOT1 nq1) ) & ( $ AND3 nq3,nq2,(NOT1 nq1) implies $ ns6 ) & ( $ ns7 implies $ AND3 nq3,nq2,nq1 ) & ( $ AND3 nq3,nq2,nq1 implies $ ns7 ) & ( $ nq1 implies $ NOT1 q1 ) & ( $ NOT1 q1 implies $ nq1 ) & ( $ nq2 implies $ XOR2 q1,q2 ) & ( $ XOR2 q1,q2 implies $ nq2 ) & ( $ nq3 implies $ OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) ) & ( $ OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3)) implies $ nq3 ) & not ( ( $ ns1 implies $ s0 ) & ( $ s0 implies $ ns1 ) & ( $ ns2 implies $ s1 ) & ( $ s1 implies $ ns2 ) & ( $ ns3 implies $ s2 ) & ( $ s2 implies $ ns3 ) & ( $ ns4 implies $ s3 ) & ( $ s3 implies $ ns4 ) & ( $ ns5 implies $ s4 ) & ( $ s4 implies $ ns5 ) & ( $ ns6 implies $ s5 ) & ( $ s5 implies $ ns6 ) & ( $ ns7 implies $ s6 ) & ( $ s6 implies $ ns7 ) & ( $ ns0 implies $ s7 ) & ( $ s7 implies $ ns0 ) ) )
proof end;

theorem :: GATE_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, d, b, c being set holds
( $ AND3 (AND2 a,d),(AND2 b,d),(AND2 c,d) iff $ AND2 (AND3 a,b,c),d )
proof end;

theorem :: GATE_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set holds
( ( not $ AND2 a,b implies $ OR2 (NOT1 a),(NOT1 b) ) & ( $ OR2 (NOT1 a),(NOT1 b) implies not $ AND2 a,b ) & ( $ OR2 a,b & $ OR2 c,b implies $ OR2 (AND2 a,c),b ) & ( $ OR2 (AND2 a,c),b implies ( $ OR2 a,b & $ OR2 c,b ) ) & ( $ OR2 a,b & $ OR2 c,b & $ OR2 d,b implies $ OR2 (AND3 a,c,d),b ) & ( $ OR2 (AND3 a,c,d),b implies ( $ OR2 a,b & $ OR2 c,b & $ OR2 d,b ) ) & not ( $ OR2 a,b & ( $ a implies $ c ) & ( $ c implies $ a ) & not $ OR2 c,b ) )
proof end;

theorem :: GATE_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3, R being set holds
not ( ( $ s0 implies $ AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) ) & ( $ AND3 (NOT1 q3),(NOT1 q2),(NOT1 q1) implies $ s0 ) & ( $ s1 implies $ AND3 (NOT1 q3),(NOT1 q2),q1 ) & ( $ AND3 (NOT1 q3),(NOT1 q2),q1 implies $ s1 ) & ( $ s2 implies $ AND3 (NOT1 q3),q2,(NOT1 q1) ) & ( $ AND3 (NOT1 q3),q2,(NOT1 q1) implies $ s2 ) & ( $ s3 implies $ AND3 (NOT1 q3),q2,q1 ) & ( $ AND3 (NOT1 q3),q2,q1 implies $ s3 ) & ( $ s4 implies $ AND3 q3,(NOT1 q2),(NOT1 q1) ) & ( $ AND3 q3,(NOT1 q2),(NOT1 q1) implies $ s4 ) & ( $ s5 implies $ AND3 q3,(NOT1 q2),q1 ) & ( $ AND3 q3,(NOT1 q2),q1 implies $ s5 ) & ( $ s6 implies $ AND3 q3,q2,(NOT1 q1) ) & ( $ AND3 q3,q2,(NOT1 q1) implies $ s6 ) & ( $ s7 implies $ AND3 q3,q2,q1 ) & ( $ AND3 q3,q2,q1 implies $ s7 ) & ( $ ns0 implies $ AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) ) & ( $ AND3 (NOT1 nq3),(NOT1 nq2),(NOT1 nq1) implies $ ns0 ) & ( $ ns1 implies $ AND3 (NOT1 nq3),(NOT1 nq2),nq1 ) & ( $ AND3 (NOT1 nq3),(NOT1 nq2),nq1 implies $ ns1 ) & ( $ ns2 implies $ AND3 (NOT1 nq3),nq2,(NOT1 nq1) ) & ( $ AND3 (NOT1 nq3),nq2,(NOT1 nq1) implies $ ns2 ) & ( $ ns3 implies $ AND3 (NOT1 nq3),nq2,nq1 ) & ( $ AND3 (NOT1 nq3),nq2,nq1 implies $ ns3 ) & ( $ ns4 implies $ AND3 nq3,(NOT1 nq2),(NOT1 nq1) ) & ( $ AND3 nq3,(NOT1 nq2),(NOT1 nq1) implies $ ns4 ) & ( $ ns5 implies $ AND3 nq3,(NOT1 nq2),nq1 ) & ( $ AND3 nq3,(NOT1 nq2),nq1 implies $ ns5 ) & ( $ ns6 implies $ AND3 nq3,nq2,(NOT1 nq1) ) & ( $ AND3 nq3,nq2,(NOT1 nq1) implies $ ns6 ) & ( $ ns7 implies $ AND3 nq3,nq2,nq1 ) & ( $ AND3 nq3,nq2,nq1 implies $ ns7 ) & ( $ nq1 implies $ AND2 (NOT1 q1),R ) & ( $ AND2 (NOT1 q1),R implies $ nq1 ) & ( $ nq2 implies $ AND2 (XOR2 q1,q2),R ) & ( $ AND2 (XOR2 q1,q2),R implies $ nq2 ) & ( $ nq3 implies $ AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),R ) & ( $ AND2 (OR2 (AND2 q3,(NOT1 q1)),(AND2 q1,(XOR2 q2,q3))),R implies $ nq3 ) & not ( ( $ ns1 implies $ AND2 s0,R ) & ( $ AND2 s0,R implies $ ns1 ) & ( $ ns2 implies $ AND2 s1,R ) & ( $ AND2 s1,R implies $ ns2 ) & ( $ ns3 implies $ AND2 s2,R ) & ( $ AND2 s2,R implies $ ns3 ) & ( $ ns4 implies $ AND2 s3,R ) & ( $ AND2 s3,R implies $ ns4 ) & ( $ ns5 implies $ AND2 s4,R ) & ( $ AND2 s4,R implies $ ns5 ) & ( $ ns6 implies $ AND2 s5,R ) & ( $ AND2 s5,R implies $ ns6 ) & ( $ ns7 implies $ AND2 s6,R ) & ( $ AND2 s6,R implies $ ns7 ) & ( $ ns0 implies $ OR2 s7,(NOT1 R) ) & ( $ OR2 s7,(NOT1 R) implies $ ns0 ) ) )
proof end;