X86 X012+X013 "Fre PodWR Fre Rfi PodRR+Fre PodWR Fre Rfi PodRR Fre PodWR Fre Rfi PodRR" {} P0 | P1 | P2 | P3 ; MOV [y],$1 | MOV [x],$1 | MOV [d],$1 | MOV [c],$1 ; MOV EAX,[x] | MOV EAX,[x] | MOV EAX,[d] | MOV EAX,[d] ; MOV [b],$1 | MOV EBX,[y] | MOV EBX,[a] | ; MOV EBX,[b] | MOV [a],$1 | | ; MOV ECX,[c] | MOV ECX,[b] | | ; forall (0:EBX=1 /\ (1:EAX=1 /\ (2:EAX=1 /\ (0:EAX=1 /\ (0:ECX=1 /\ (1:EBX=1 /\ (1:ECX=1 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)) \/ 1:ECX=0 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0))) \/ 1:EBX=0 /\ (1:ECX=1 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)) \/ 1:ECX=0 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)))) \/ 0:ECX=0 /\ (1:EBX=1 /\ (1:ECX=1 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)) \/ 1:ECX=0 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1))) \/ 1:EBX=0 /\ (1:ECX=1 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)) \/ 1:ECX=0 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1))))) \/ 0:EAX=0 /\ (1:EBX=1 /\ (0:ECX=1 /\ (1:ECX=1 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)) \/ 1:ECX=0 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0))) \/ 0:ECX=0 /\ (1:ECX=1 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1 \/ 3:EAX=0)) \/ 1:ECX=0 /\ (2:EBX=1 /\ (3:EAX=1 \/ 3:EAX=0) \/ 2:EBX=0 /\ (3:EAX=1)))))))))