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

theorem :: GATE_3: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, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2 being set holds
not ( ( $ s0 implies $ AND2 (NOT1 q2),(NOT1 q1) ) & ( $ AND2 (NOT1 q2),(NOT1 q1) implies $ s0 ) & ( $ s1 implies $ AND2 (NOT1 q2),q1 ) & ( $ AND2 (NOT1 q2),q1 implies $ s1 ) & ( $ s2 implies $ AND2 q2,(NOT1 q1) ) & ( $ AND2 q2,(NOT1 q1) implies $ s2 ) & ( $ s3 implies $ AND2 q2,q1 ) & ( $ AND2 q2,q1 implies $ s3 ) & ( $ ns0 implies $ AND2 (NOT1 nq2),(NOT1 nq1) ) & ( $ AND2 (NOT1 nq2),(NOT1 nq1) implies $ ns0 ) & ( $ ns1 implies $ AND2 (NOT1 nq2),nq1 ) & ( $ AND2 (NOT1 nq2),nq1 implies $ ns1 ) & ( $ ns2 implies $ AND2 nq2,(NOT1 nq1) ) & ( $ AND2 nq2,(NOT1 nq1) implies $ ns2 ) & ( $ ns3 implies $ AND2 nq2,nq1 ) & ( $ AND2 nq2,nq1 implies $ ns3 ) & ( $ nq1 implies $ NOT1 q2 ) & ( $ NOT1 q2 implies $ nq1 ) & ( $ nq2 implies $ q1 ) & ( $ q1 implies $ nq2 ) & not ( ( $ ns1 implies $ s0 ) & ( $ s0 implies $ ns1 ) & ( $ ns3 implies $ s1 ) & ( $ s1 implies $ ns3 ) & ( $ ns2 implies $ s3 ) & ( $ s3 implies $ ns2 ) & ( $ ns0 implies $ s2 ) & ( $ s2 implies $ ns0 ) ) )
proof end;

theorem :: GATE_3:2  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, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2, R being set holds
not ( ( $ s0 implies $ AND2 (NOT1 q2),(NOT1 q1) ) & ( $ AND2 (NOT1 q2),(NOT1 q1) implies $ s0 ) & ( $ s1 implies $ AND2 (NOT1 q2),q1 ) & ( $ AND2 (NOT1 q2),q1 implies $ s1 ) & ( $ s2 implies $ AND2 q2,(NOT1 q1) ) & ( $ AND2 q2,(NOT1 q1) implies $ s2 ) & ( $ s3 implies $ AND2 q2,q1 ) & ( $ AND2 q2,q1 implies $ s3 ) & ( $ ns0 implies $ AND2 (NOT1 nq2),(NOT1 nq1) ) & ( $ AND2 (NOT1 nq2),(NOT1 nq1) implies $ ns0 ) & ( $ ns1 implies $ AND2 (NOT1 nq2),nq1 ) & ( $ AND2 (NOT1 nq2),nq1 implies $ ns1 ) & ( $ ns2 implies $ AND2 nq2,(NOT1 nq1) ) & ( $ AND2 nq2,(NOT1 nq1) implies $ ns2 ) & ( $ ns3 implies $ AND2 nq2,nq1 ) & ( $ AND2 nq2,nq1 implies $ ns3 ) & ( $ nq1 implies $ AND2 (NOT1 q2),R ) & ( $ AND2 (NOT1 q2),R implies $ nq1 ) & ( $ nq2 implies $ AND2 q1,R ) & ( $ AND2 q1,R implies $ nq2 ) & not ( ( $ ns1 implies $ AND2 s0,R ) & ( $ AND2 s0,R implies $ ns1 ) & ( $ ns3 implies $ AND2 s1,R ) & ( $ AND2 s1,R implies $ ns3 ) & ( $ ns2 implies $ AND2 s3,R ) & ( $ AND2 s3,R implies $ ns2 ) & ( $ ns0 implies $ OR2 (AND2 s2,R),(NOT1 R) ) & ( $ OR2 (AND2 s2,R),(NOT1 R) implies $ ns0 ) ) )
proof end;

theorem :: GATE_3:3  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 q3 ) & ( $ NOT1 q3 implies $ nq1 ) & ( $ nq2 implies $ q1 ) & ( $ q1 implies $ nq2 ) & ( $ nq3 implies $ q2 ) & ( $ q2 implies $ nq3 ) & not ( ( $ ns1 implies $ s0 ) & ( $ s0 implies $ ns1 ) & ( $ ns3 implies $ s1 ) & ( $ s1 implies $ ns3 ) & ( $ ns7 implies $ s3 ) & ( $ s3 implies $ ns7 ) & ( $ ns6 implies $ s7 ) & ( $ s7 implies $ ns6 ) & ( $ ns4 implies $ s6 ) & ( $ s6 implies $ ns4 ) & ( $ ns0 implies $ s4 ) & ( $ s4 implies $ ns0 ) & ( $ ns2 implies $ s5 ) & ( $ s5 implies $ ns2 ) & ( $ ns5 implies $ s2 ) & ( $ s2 implies $ ns5 ) ) )
proof end;

theorem :: GATE_3: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 q3),R ) & ( $ AND2 (NOT1 q3),R implies $ nq1 ) & ( $ nq2 implies $ AND2 q1,R ) & ( $ AND2 q1,R implies $ nq2 ) & ( $ nq3 implies $ AND2 q2,R ) & ( $ AND2 q2,R implies $ nq3 ) & not ( ( $ ns1 implies $ AND2 s0,R ) & ( $ AND2 s0,R implies $ ns1 ) & ( $ ns3 implies $ AND2 s1,R ) & ( $ AND2 s1,R implies $ ns3 ) & ( $ ns7 implies $ AND2 s3,R ) & ( $ AND2 s3,R implies $ ns7 ) & ( $ ns6 implies $ AND2 s7,R ) & ( $ AND2 s7,R implies $ ns6 ) & ( $ ns4 implies $ AND2 s6,R ) & ( $ AND2 s6,R implies $ ns4 ) & ( $ ns0 implies $ OR2 (AND2 s4,R),(NOT1 R) ) & ( $ OR2 (AND2 s4,R),(NOT1 R) implies $ ns0 ) & ( $ ns2 implies $ AND2 s5,R ) & ( $ AND2 s5,R implies $ ns2 ) & ( $ ns5 implies $ AND2 s2,R ) & ( $ AND2 s2,R implies $ ns5 ) ) )
proof end;

theorem :: GATE_3:5  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, s8, s9, s10, s11, s12, s13, s14, s15, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, ns8, ns9, ns10, ns11, ns12, ns13, ns14, ns15, q1, q2, q3, q4, nq1, nq2, nq3, nq4 being set holds
not ( ( $ s0 implies $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1) ) & ( $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1) implies $ s0 ) & ( $ s1 implies $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),q1 ) & ( $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),q1 implies $ s1 ) & ( $ s2 implies $ AND4 (NOT1 q4),(NOT1 q3),q2,(NOT1 q1) ) & ( $ AND4 (NOT1 q4),(NOT1 q3),q2,(NOT1 q1) implies $ s2 ) & ( $ s3 implies $ AND4 (NOT1 q4),(NOT1 q3),q2,q1 ) & ( $ AND4 (NOT1 q4),(NOT1 q3),q2,q1 implies $ s3 ) & ( $ s4 implies $ AND4 (NOT1 q4),q3,(NOT1 q2),(NOT1 q1) ) & ( $ AND4 (NOT1 q4),q3,(NOT1 q2),(NOT1 q1) implies $ s4 ) & ( $ s5 implies $ AND4 (NOT1 q4),q3,(NOT1 q2),q1 ) & ( $ AND4 (NOT1 q4),q3,(NOT1 q2),q1 implies $ s5 ) & ( $ s6 implies $ AND4 (NOT1 q4),q3,q2,(NOT1 q1) ) & ( $ AND4 (NOT1 q4),q3,q2,(NOT1 q1) implies $ s6 ) & ( $ s7 implies $ AND4 (NOT1 q4),q3,q2,q1 ) & ( $ AND4 (NOT1 q4),q3,q2,q1 implies $ s7 ) & ( $ s8 implies $ AND4 q4,(NOT1 q3),(NOT1 q2),(NOT1 q1) ) & ( $ AND4 q4,(NOT1 q3),(NOT1 q2),(NOT1 q1) implies $ s8 ) & ( $ s9 implies $ AND4 q4,(NOT1 q3),(NOT1 q2),q1 ) & ( $ AND4 q4,(NOT1 q3),(NOT1 q2),q1 implies $ s9 ) & ( $ s10 implies $ AND4 q4,(NOT1 q3),q2,(NOT1 q1) ) & ( $ AND4 q4,(NOT1 q3),q2,(NOT1 q1) implies $ s10 ) & ( $ s11 implies $ AND4 q4,(NOT1 q3),q2,q1 ) & ( $ AND4 q4,(NOT1 q3),q2,q1 implies $ s11 ) & ( $ s12 implies $ AND4 q4,q3,(NOT1 q2),(NOT1 q1) ) & ( $ AND4 q4,q3,(NOT1 q2),(NOT1 q1) implies $ s12 ) & ( $ s13 implies $ AND4 q4,q3,(NOT1 q2),q1 ) & ( $ AND4 q4,q3,(NOT1 q2),q1 implies $ s13 ) & ( $ s14 implies $ AND4 q4,q3,q2,(NOT1 q1) ) & ( $ AND4 q4,q3,q2,(NOT1 q1) implies $ s14 ) & ( $ s15 implies $ AND4 q4,q3,q2,q1 ) & ( $ AND4 q4,q3,q2,q1 implies $ s15 ) & ( $ ns0 implies $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) implies $ ns0 ) & ( $ ns1 implies $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1 ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1 implies $ ns1 ) & ( $ ns2 implies $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1) implies $ ns2 ) & ( $ ns3 implies $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,nq1 ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,nq1 implies $ ns3 ) & ( $ ns4 implies $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1) implies $ ns4 ) & ( $ ns5 implies $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),nq1 ) & ( $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),nq1 implies $ ns5 ) & ( $ ns6 implies $ AND4 (NOT1 nq4),nq3,nq2,(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),nq3,nq2,(NOT1 nq1) implies $ ns6 ) & ( $ ns7 implies $ AND4 (NOT1 nq4),nq3,nq2,nq1 ) & ( $ AND4 (NOT1 nq4),nq3,nq2,nq1 implies $ ns7 ) & ( $ ns8 implies $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) implies $ ns8 ) & ( $ ns9 implies $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),nq1 ) & ( $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),nq1 implies $ ns9 ) & ( $ ns10 implies $ AND4 nq4,(NOT1 nq3),nq2,(NOT1 nq1) ) & ( $ AND4 nq4,(NOT1 nq3),nq2,(NOT1 nq1) implies $ ns10 ) & ( $ ns11 implies $ AND4 nq4,(NOT1 nq3),nq2,nq1 ) & ( $ AND4 nq4,(NOT1 nq3),nq2,nq1 implies $ ns11 ) & ( $ ns12 implies $ AND4 nq4,nq3,(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 nq4,nq3,(NOT1 nq2),(NOT1 nq1) implies $ ns12 ) & ( $ ns13 implies $ AND4 nq4,nq3,(NOT1 nq2),nq1 ) & ( $ AND4 nq4,nq3,(NOT1 nq2),nq1 implies $ ns13 ) & ( $ ns14 implies $ AND4 nq4,nq3,nq2,(NOT1 nq1) ) & ( $ AND4 nq4,nq3,nq2,(NOT1 nq1) implies $ ns14 ) & ( $ ns15 implies $ AND4 nq4,nq3,nq2,nq1 ) & ( $ AND4 nq4,nq3,nq2,nq1 implies $ ns15 ) & ( $ nq1 implies $ NOT1 q4 ) & ( $ NOT1 q4 implies $ nq1 ) & ( $ nq2 implies $ q1 ) & ( $ q1 implies $ nq2 ) & ( $ nq3 implies $ q2 ) & ( $ q2 implies $ nq3 ) & ( $ nq4 implies $ q3 ) & ( $ q3 implies $ nq4 ) & not ( ( $ ns1 implies $ s0 ) & ( $ s0 implies $ ns1 ) & ( $ ns3 implies $ s1 ) & ( $ s1 implies $ ns3 ) & ( $ ns7 implies $ s3 ) & ( $ s3 implies $ ns7 ) & ( $ ns15 implies $ s7 ) & ( $ s7 implies $ ns15 ) & ( $ ns14 implies $ s15 ) & ( $ s15 implies $ ns14 ) & ( $ ns12 implies $ s14 ) & ( $ s14 implies $ ns12 ) & ( $ ns8 implies $ s12 ) & ( $ s12 implies $ ns8 ) & ( $ ns0 implies $ s8 ) & ( $ s8 implies $ ns0 ) & ( $ ns5 implies $ s2 ) & ( $ s2 implies $ ns5 ) & ( $ ns11 implies $ s5 ) & ( $ s5 implies $ ns11 ) & ( $ ns6 implies $ s11 ) & ( $ s11 implies $ ns6 ) & ( $ ns13 implies $ s6 ) & ( $ s6 implies $ ns13 ) & ( $ ns10 implies $ s13 ) & ( $ s13 implies $ ns10 ) & ( $ ns4 implies $ s10 ) & ( $ s10 implies $ ns4 ) & ( $ ns9 implies $ s4 ) & ( $ s4 implies $ ns9 ) & ( $ ns2 implies $ s9 ) & ( $ s9 implies $ ns2 ) ) )
proof end;

theorem :: GATE_3:6  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, s8, s9, s10, s11, s12, s13, s14, s15, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, ns8, ns9, ns10, ns11, ns12, ns13, ns14, ns15, q1, q2, q3, q4, nq1, nq2, nq3, nq4, R being set holds
not ( ( $ s0 implies $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1) ) & ( $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),(NOT1 q1) implies $ s0 ) & ( $ s1 implies $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),q1 ) & ( $ AND4 (NOT1 q4),(NOT1 q3),(NOT1 q2),q1 implies $ s1 ) & ( $ s2 implies $ AND4 (NOT1 q4),(NOT1 q3),q2,(NOT1 q1) ) & ( $ AND4 (NOT1 q4),(NOT1 q3),q2,(NOT1 q1) implies $ s2 ) & ( $ s3 implies $ AND4 (NOT1 q4),(NOT1 q3),q2,q1 ) & ( $ AND4 (NOT1 q4),(NOT1 q3),q2,q1 implies $ s3 ) & ( $ s4 implies $ AND4 (NOT1 q4),q3,(NOT1 q2),(NOT1 q1) ) & ( $ AND4 (NOT1 q4),q3,(NOT1 q2),(NOT1 q1) implies $ s4 ) & ( $ s5 implies $ AND4 (NOT1 q4),q3,(NOT1 q2),q1 ) & ( $ AND4 (NOT1 q4),q3,(NOT1 q2),q1 implies $ s5 ) & ( $ s6 implies $ AND4 (NOT1 q4),q3,q2,(NOT1 q1) ) & ( $ AND4 (NOT1 q4),q3,q2,(NOT1 q1) implies $ s6 ) & ( $ s7 implies $ AND4 (NOT1 q4),q3,q2,q1 ) & ( $ AND4 (NOT1 q4),q3,q2,q1 implies $ s7 ) & ( $ s8 implies $ AND4 q4,(NOT1 q3),(NOT1 q2),(NOT1 q1) ) & ( $ AND4 q4,(NOT1 q3),(NOT1 q2),(NOT1 q1) implies $ s8 ) & ( $ s9 implies $ AND4 q4,(NOT1 q3),(NOT1 q2),q1 ) & ( $ AND4 q4,(NOT1 q3),(NOT1 q2),q1 implies $ s9 ) & ( $ s10 implies $ AND4 q4,(NOT1 q3),q2,(NOT1 q1) ) & ( $ AND4 q4,(NOT1 q3),q2,(NOT1 q1) implies $ s10 ) & ( $ s11 implies $ AND4 q4,(NOT1 q3),q2,q1 ) & ( $ AND4 q4,(NOT1 q3),q2,q1 implies $ s11 ) & ( $ s12 implies $ AND4 q4,q3,(NOT1 q2),(NOT1 q1) ) & ( $ AND4 q4,q3,(NOT1 q2),(NOT1 q1) implies $ s12 ) & ( $ s13 implies $ AND4 q4,q3,(NOT1 q2),q1 ) & ( $ AND4 q4,q3,(NOT1 q2),q1 implies $ s13 ) & ( $ s14 implies $ AND4 q4,q3,q2,(NOT1 q1) ) & ( $ AND4 q4,q3,q2,(NOT1 q1) implies $ s14 ) & ( $ s15 implies $ AND4 q4,q3,q2,q1 ) & ( $ AND4 q4,q3,q2,q1 implies $ s15 ) & ( $ ns0 implies $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) implies $ ns0 ) & ( $ ns1 implies $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1 ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),(NOT1 nq2),nq1 implies $ ns1 ) & ( $ ns2 implies $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,(NOT1 nq1) implies $ ns2 ) & ( $ ns3 implies $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,nq1 ) & ( $ AND4 (NOT1 nq4),(NOT1 nq3),nq2,nq1 implies $ ns3 ) & ( $ ns4 implies $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),(NOT1 nq1) implies $ ns4 ) & ( $ ns5 implies $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),nq1 ) & ( $ AND4 (NOT1 nq4),nq3,(NOT1 nq2),nq1 implies $ ns5 ) & ( $ ns6 implies $ AND4 (NOT1 nq4),nq3,nq2,(NOT1 nq1) ) & ( $ AND4 (NOT1 nq4),nq3,nq2,(NOT1 nq1) implies $ ns6 ) & ( $ ns7 implies $ AND4 (NOT1 nq4),nq3,nq2,nq1 ) & ( $ AND4 (NOT1 nq4),nq3,nq2,nq1 implies $ ns7 ) & ( $ ns8 implies $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),(NOT1 nq1) implies $ ns8 ) & ( $ ns9 implies $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),nq1 ) & ( $ AND4 nq4,(NOT1 nq3),(NOT1 nq2),nq1 implies $ ns9 ) & ( $ ns10 implies $ AND4 nq4,(NOT1 nq3),nq2,(NOT1 nq1) ) & ( $ AND4 nq4,(NOT1 nq3),nq2,(NOT1 nq1) implies $ ns10 ) & ( $ ns11 implies $ AND4 nq4,(NOT1 nq3),nq2,nq1 ) & ( $ AND4 nq4,(NOT1 nq3),nq2,nq1 implies $ ns11 ) & ( $ ns12 implies $ AND4 nq4,nq3,(NOT1 nq2),(NOT1 nq1) ) & ( $ AND4 nq4,nq3,(NOT1 nq2),(NOT1 nq1) implies $ ns12 ) & ( $ ns13 implies $ AND4 nq4,nq3,(NOT1 nq2),nq1 ) & ( $ AND4 nq4,nq3,(NOT1 nq2),nq1 implies $ ns13 ) & ( $ ns14 implies $ AND4 nq4,nq3,nq2,(NOT1 nq1) ) & ( $ AND4 nq4,nq3,nq2,(NOT1 nq1) implies $ ns14 ) & ( $ ns15 implies $ AND4 nq4,nq3,nq2,nq1 ) & ( $ AND4 nq4,nq3,nq2,nq1 implies $ ns15 ) & ( $ nq1 implies $ AND2 (NOT1 q4),R ) & ( $ AND2 (NOT1 q4),R implies $ nq1 ) & ( $ nq2 implies $ AND2 q1,R ) & ( $ AND2 q1,R implies $ nq2 ) & ( $ nq3 implies $ AND2 q2,R ) & ( $ AND2 q2,R implies $ nq3 ) & ( $ nq4 implies $ AND2 q3,R ) & ( $ AND2 q3,R implies $ nq4 ) & not ( ( $ ns1 implies $ AND2 s0,R ) & ( $ AND2 s0,R implies $ ns1 ) & ( $ ns3 implies $ AND2 s1,R ) & ( $ AND2 s1,R implies $ ns3 ) & ( $ ns7 implies $ AND2 s3,R ) & ( $ AND2 s3,R implies $ ns7 ) & ( $ ns15 implies $ AND2 s7,R ) & ( $ AND2 s7,R implies $ ns15 ) & ( $ ns14 implies $ AND2 s15,R ) & ( $ AND2 s15,R implies $ ns14 ) & ( $ ns12 implies $ AND2 s14,R ) & ( $ AND2 s14,R implies $ ns12 ) & ( $ ns8 implies $ AND2 s12,R ) & ( $ AND2 s12,R implies $ ns8 ) & ( $ ns0 implies $ OR2 (AND2 s8,R),(NOT1 R) ) & ( $ OR2 (AND2 s8,R),(NOT1 R) implies $ ns0 ) & ( $ ns5 implies $ AND2 s2,R ) & ( $ AND2 s2,R implies $ ns5 ) & ( $ ns11 implies $ AND2 s5,R ) & ( $ AND2 s5,R implies $ ns11 ) & ( $ ns6 implies $ AND2 s11,R ) & ( $ AND2 s11,R implies $ ns6 ) & ( $ ns13 implies $ AND2 s6,R ) & ( $ AND2 s6,R implies $ ns13 ) & ( $ ns10 implies $ AND2 s13,R ) & ( $ AND2 s13,R implies $ ns10 ) & ( $ ns4 implies $ AND2 s10,R ) & ( $ AND2 s10,R implies $ ns4 ) & ( $ ns9 implies $ AND2 s4,R ) & ( $ AND2 s4,R implies $ ns9 ) & ( $ ns2 implies $ AND2 s9,R ) & ( $ AND2 s9,R implies $ ns2 ) ) )
proof end;