proof (prove) using this: 0 ≤ pmf (sds R1) a ∧ 0 ≤ pmf (sds R1) b ∧ 0 ≤ pmf (sds R1) c ∧ 0 ≤ pmf (sds R1) d 0 ≤ pmf (sds R2) a ∧ 0 ≤ pmf (sds R2) b ∧ 0 ≤ pmf (sds R2) c ∧ 0 ≤ pmf (sds R2) d 0 ≤ pmf (sds R3) a ∧ 0 ≤ pmf (sds R3) b ∧ 0 ≤ pmf (sds R3) c ∧ 0 ≤ pmf (sds R3) d 0 ≤ pmf (sds R4) a ∧ 0 ≤ pmf (sds R4) b ∧ 0 ≤ pmf (sds R4) c ∧ 0 ≤ pmf (sds R4) d 0 ≤ pmf (sds R5) a ∧ 0 ≤ pmf (sds R5) b ∧ 0 ≤ pmf (sds R5) c ∧ 0 ≤ pmf (sds R5) d 0 ≤ pmf (sds R6) a ∧ 0 ≤ pmf (sds R6) b ∧ 0 ≤ pmf (sds R6) c ∧ 0 ≤ pmf (sds R6) d 0 ≤ pmf (sds R7) a ∧ 0 ≤ pmf (sds R7) b ∧ 0 ≤ pmf (sds R7) c ∧ 0 ≤ pmf (sds R7) d 0 ≤ pmf (sds R8) a ∧ 0 ≤ pmf (sds R8) b ∧ 0 ≤ pmf (sds R8) c ∧ 0 ≤ pmf (sds R8) d 0 ≤ pmf (sds R9) a ∧ 0 ≤ pmf (sds R9) b ∧ 0 ≤ pmf (sds R9) c ∧ 0 ≤ pmf (sds R9) d 0 ≤ pmf (sds R10) a ∧ 0 ≤ pmf (sds R10) b ∧ 0 ≤ pmf (sds R10) c ∧ 0 ≤ pmf (sds R10) d 0 ≤ pmf (sds R11) a ∧ 0 ≤ pmf (sds R11) b ∧ 0 ≤ pmf (sds R11) c ∧ 0 ≤ pmf (sds R11) d 0 ≤ pmf (sds R12) a ∧ 0 ≤ pmf (sds R12) b ∧ 0 ≤ pmf (sds R12) c ∧ 0 ≤ pmf (sds R12) d 0 ≤ pmf (sds R13) a ∧ 0 ≤ pmf (sds R13) b ∧ 0 ≤ pmf (sds R13) c ∧ 0 ≤ pmf (sds R13) d 0 ≤ pmf (sds R14) a ∧ 0 ≤ pmf (sds R14) b ∧ 0 ≤ pmf (sds R14) c ∧ 0 ≤ pmf (sds R14) d 0 ≤ pmf (sds R15) a ∧ 0 ≤ pmf (sds R15) b ∧ 0 ≤ pmf (sds R15) c ∧ 0 ≤ pmf (sds R15) d 0 ≤ pmf (sds R16) a ∧ 0 ≤ pmf (sds R16) b ∧ 0 ≤ pmf (sds R16) c ∧ 0 ≤ pmf (sds R16) d 0 ≤ pmf (sds R17) a ∧ 0 ≤ pmf (sds R17) b ∧ 0 ≤ pmf (sds R17) c ∧ 0 ≤ pmf (sds R17) d 0 ≤ pmf (sds R18) a ∧ 0 ≤ pmf (sds R18) b ∧ 0 ≤ pmf (sds R18) c ∧ 0 ≤ pmf (sds R18) d 0 ≤ pmf (sds R19) a ∧ 0 ≤ pmf (sds R19) b ∧ 0 ≤ pmf (sds R19) c ∧ 0 ≤ pmf (sds R19) d 0 ≤ pmf (sds R20) a ∧ 0 ≤ pmf (sds R20) b ∧ 0 ≤ pmf (sds R20) c ∧ 0 ≤ pmf (sds R20) d 0 ≤ pmf (sds R21) a ∧ 0 ≤ pmf (sds R21) b ∧ 0 ≤ pmf (sds R21) c ∧ 0 ≤ pmf (sds R21) d 0 ≤ pmf (sds R22) a ∧ 0 ≤ pmf (sds R22) b ∧ 0 ≤ pmf (sds R22) c ∧ 0 ≤ pmf (sds R22) d 0 ≤ pmf (sds R23) a ∧ 0 ≤ pmf (sds R23) b ∧ 0 ≤ pmf (sds R23) c ∧ 0 ≤ pmf (sds R23) d 0 ≤ pmf (sds R24) a ∧ 0 ≤ pmf (sds R24) b ∧ 0 ≤ pmf (sds R24) c ∧ 0 ≤ pmf (sds R24) d 0 ≤ pmf (sds R25) a ∧ 0 ≤ pmf (sds R25) b ∧ 0 ≤ pmf (sds R25) c ∧ 0 ≤ pmf (sds R25) d 0 ≤ pmf (sds R26) a ∧ 0 ≤ pmf (sds R26) b ∧ 0 ≤ pmf (sds R26) c ∧ 0 ≤ pmf (sds R26) d 0 ≤ pmf (sds R27) a ∧ 0 ≤ pmf (sds R27) b ∧ 0 ≤ pmf (sds R27) c ∧ 0 ≤ pmf (sds R27) d 0 ≤ pmf (sds R28) a ∧ 0 ≤ pmf (sds R28) b ∧ 0 ≤ pmf (sds R28) c ∧ 0 ≤ pmf (sds R28) d 0 ≤ pmf (sds R29) a ∧ 0 ≤ pmf (sds R29) b ∧ 0 ≤ pmf (sds R29) c ∧ 0 ≤ pmf (sds R29) d 0 ≤ pmf (sds R30) a ∧ 0 ≤ pmf (sds R30) b ∧ 0 ≤ pmf (sds R30) c ∧ 0 ≤ pmf (sds R30) d 0 ≤ pmf (sds R31) a ∧ 0 ≤ pmf (sds R31) b ∧ 0 ≤ pmf (sds R31) c ∧ 0 ≤ pmf (sds R31) d 0 ≤ pmf (sds R32) a ∧ 0 ≤ pmf (sds R32) b ∧ 0 ≤ pmf (sds R32) c ∧ 0 ≤ pmf (sds R32) d 0 ≤ pmf (sds R33) a ∧ 0 ≤ pmf (sds R33) b ∧ 0 ≤ pmf (sds R33) c ∧ 0 ≤ pmf (sds R33) d 0 ≤ pmf (sds R34) a ∧ 0 ≤ pmf (sds R34) b ∧ 0 ≤ pmf (sds R34) c ∧ 0 ≤ pmf (sds R34) d 0 ≤ pmf (sds R35) a ∧ 0 ≤ pmf (sds R35) b ∧ 0 ≤ pmf (sds R35) c ∧ 0 ≤ pmf (sds R35) d 0 ≤ pmf (sds R36) a ∧ 0 ≤ pmf (sds R36) b ∧ 0 ≤ pmf (sds R36) c ∧ 0 ≤ pmf (sds R36) d 0 ≤ pmf (sds R37) a ∧ 0 ≤ pmf (sds R37) b ∧ 0 ≤ pmf (sds R37) c ∧ 0 ≤ pmf (sds R37) d 0 ≤ pmf (sds R38) a ∧ 0 ≤ pmf (sds R38) b ∧ 0 ≤ pmf (sds R38) c ∧ 0 ≤ pmf (sds R38) d 0 ≤ pmf (sds R39) a ∧ 0 ≤ pmf (sds R39) b ∧ 0 ≤ pmf (sds R39) c ∧ 0 ≤ pmf (sds R39) d 0 ≤ pmf (sds R40) a ∧ 0 ≤ pmf (sds R40) b ∧ 0 ≤ pmf (sds R40) c ∧ 0 ≤ pmf (sds R40) d 0 ≤ pmf (sds R41) a ∧ 0 ≤ pmf (sds R41) b ∧ 0 ≤ pmf (sds R41) c ∧ 0 ≤ pmf (sds R41) d 0 ≤ pmf (sds R42) a ∧ 0 ≤ pmf (sds R42) b ∧ 0 ≤ pmf (sds R42) c ∧ 0 ≤ pmf (sds R42) d 0 ≤ pmf (sds R43) a ∧ 0 ≤ pmf (sds R43) b ∧ 0 ≤ pmf (sds R43) c ∧ 0 ≤ pmf (sds R43) d 0 ≤ pmf (sds R44) a ∧ 0 ≤ pmf (sds R44) b ∧ 0 ≤ pmf (sds R44) c ∧ 0 ≤ pmf (sds R44) d 0 ≤ pmf (sds R45) a ∧ 0 ≤ pmf (sds R45) b ∧ 0 ≤ pmf (sds R45) c ∧ 0 ≤ pmf (sds R45) d 0 ≤ pmf (sds R46) a ∧ 0 ≤ pmf (sds R46) b ∧ 0 ≤ pmf (sds R46) c ∧ 0 ≤ pmf (sds R46) d 0 ≤ pmf (sds R47) a ∧ 0 ≤ pmf (sds R47) b ∧ 0 ≤ pmf (sds R47) c ∧ 0 ≤ pmf (sds R47) d pmf (sds R1) a + pmf (sds R1) b + pmf (sds R1) c + pmf (sds R1) d = 1 pmf (sds R2) a + pmf (sds R2) b + pmf (sds R2) c + pmf (sds R2) d = 1 pmf (sds R3) a + pmf (sds R3) b + pmf (sds R3) c + pmf (sds R3) d = 1 pmf (sds R4) a + pmf (sds R4) b + pmf (sds R4) c + pmf (sds R4) d = 1 pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1 pmf (sds R6) a + pmf (sds R6) b + pmf (sds R6) c + pmf (sds R6) d = 1 pmf (sds R7) a + pmf (sds R7) b + pmf (sds R7) c + pmf (sds R7) d = 1 pmf (sds R8) a + pmf (sds R8) b + pmf (sds R8) c + pmf (sds R8) d = 1 pmf (sds R9) a + pmf (sds R9) b + pmf (sds R9) c + pmf (sds R9) d = 1 pmf (sds R10) a + pmf (sds R10) b + pmf (sds R10) c + pmf (sds R10) d = 1 pmf (sds R11) a + pmf (sds R11) b + pmf (sds R11) c + pmf (sds R11) d = 1 pmf (sds R12) a + pmf (sds R12) b + pmf (sds R12) c + pmf (sds R12) d = 1 pmf (sds R13) a + pmf (sds R13) b + pmf (sds R13) c + pmf (sds R13) d = 1 pmf (sds R14) a + pmf (sds R14) b + pmf (sds R14) c + pmf (sds R14) d = 1 pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1 pmf (sds R16) a + pmf (sds R16) b + pmf (sds R16) c + pmf (sds R16) d = 1 pmf (sds R17) a + pmf (sds R17) b + pmf (sds R17) c + pmf (sds R17) d = 1 pmf (sds R18) a + pmf (sds R18) b + pmf (sds R18) c + pmf (sds R18) d = 1 pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1 pmf (sds R20) a + pmf (sds R20) b + pmf (sds R20) c + pmf (sds R20) d = 1 pmf (sds R21) a + pmf (sds R21) b + pmf (sds R21) c + pmf (sds R21) d = 1 pmf (sds R22) a + pmf (sds R22) b + pmf (sds R22) c + pmf (sds R22) d = 1 pmf (sds R23) a + pmf (sds R23) b + pmf (sds R23) c + pmf (sds R23) d = 1 pmf (sds R24) a + pmf (sds R24) b + pmf (sds R24) c + pmf (sds R24) d = 1 pmf (sds R25) a + pmf (sds R25) b + pmf (sds R25) c + pmf (sds R25) d = 1 pmf (sds R26) a + pmf (sds R26) b + pmf (sds R26) c + pmf (sds R26) d = 1 pmf (sds R27) a + pmf (sds R27) b + pmf (sds R27) c + pmf (sds R27) d = 1 pmf (sds R28) a + pmf (sds R28) b + pmf (sds R28) c + pmf (sds R28) d = 1 pmf (sds R29) a + pmf (sds R29) b + pmf (sds R29) c + pmf (sds R29) d = 1 pmf (sds R30) a + pmf (sds R30) b + pmf (sds R30) c + pmf (sds R30) d = 1 pmf (sds R31) a + pmf (sds R31) b + pmf (sds R31) c + pmf (sds R31) d = 1 pmf (sds R32) a + pmf (sds R32) b + pmf (sds R32) c + pmf (sds R32) d = 1 pmf (sds R33) a + pmf (sds R33) b + pmf (sds R33) c + pmf (sds R33) d = 1 pmf (sds R34) a + pmf (sds R34) b + pmf (sds R34) c + pmf (sds R34) d = 1 pmf (sds R35) a + pmf (sds R35) b + pmf (sds R35) c + pmf (sds R35) d = 1 pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1 pmf (sds R37) a + pmf (sds R37) b + pmf (sds R37) c + pmf (sds R37) d = 1 pmf (sds R38) a + pmf (sds R38) b + pmf (sds R38) c + pmf (sds R38) d = 1 pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1 pmf (sds R40) a + pmf (sds R40) b + pmf (sds R40) c + pmf (sds R40) d = 1 pmf (sds R41) a + pmf (sds R41) b + pmf (sds R41) c + pmf (sds R41) d = 1 pmf (sds R42) a + pmf (sds R42) b + pmf (sds R42) c + pmf (sds R42) d = 1 pmf (sds R43) a + pmf (sds R43) b + pmf (sds R43) c + pmf (sds R43) d = 1 pmf (sds R44) a + pmf (sds R44) b + pmf (sds R44) c + pmf (sds R44) d = 1 pmf (sds R45) a + pmf (sds R45) b + pmf (sds R45) c + pmf (sds R45) d = 1 pmf (sds R46) a + pmf (sds R46) b + pmf (sds R46) c + pmf (sds R46) d = 1 pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1 pmf (sds R10) d = pmf (sds R10) a pmf (sds R10) c = pmf (sds R10) b pmf (sds R26) c = pmf (sds R26) b pmf (sds R27) c = pmf (sds R27) b pmf (sds R28) b = pmf (sds R28) c pmf (sds R29) b = pmf (sds R29) c pmf (sds R29) d = pmf (sds R29) a pmf (sds R37) d = pmf (sds R37) b pmf (sds R37) c = pmf (sds R37) a pmf (sds R43) d = pmf (sds R43) a pmf (sds R43) c = pmf (sds R43) b pmf (sds R45) c = pmf (sds R45) a pmf (sds R45) d = pmf (sds R45) a pmf (sds R45) b = pmf (sds R45) a pmf (sds R1) b = 0 ∨ pmf (sds R1) c = 0 pmf (sds R2) b = 0 ∨ pmf (sds R2) c = 0 pmf (sds R3) b = 0 pmf (sds R4) b = 0 pmf (sds R5) b = 0 pmf (sds R6) c = 0 ∨ pmf (sds R6) b = 0 pmf (sds R7) b = 0 pmf (sds R8) b = 0 pmf (sds R9) b = 0 pmf (sds R10) c = 0 ∨ pmf (sds R10) b = 0 pmf (sds R11) b = 0 pmf (sds R12) b = 0 pmf (sds R13) b = 0 ∨ pmf (sds R13) c = 0 pmf (sds R14) b = 0 pmf (sds R15) c = 0 ∨ pmf (sds R15) b = 0 pmf (sds R16) b = 0 pmf (sds R17) b = 0 pmf (sds R18) b = 0 pmf (sds R19) c = 0 ∨ pmf (sds R19) b = 0 pmf (sds R21) b = 0 pmf (sds R22) b = 0 pmf (sds R23) b = 0 pmf (sds R25) b = 0 ∨ pmf (sds R25) c = 0 pmf (sds R26) c = 0 ∨ pmf (sds R26) b = 0 pmf (sds R27) c = 0 ∨ pmf (sds R27) b = 0 pmf (sds R28) b = 0 ∨ pmf (sds R28) c = 0 pmf (sds R29) b = 0 ∨ pmf (sds R29) c = 0 pmf (sds R30) b = 0 pmf (sds R32) b = 0 pmf (sds R33) b = 0 pmf (sds R35) b = 0 pmf (sds R36) b = 0 ∨ pmf (sds R36) c = 0 pmf (sds R39) b = 0 ∨ pmf (sds R39) c = 0 pmf (sds R40) b = 0 pmf (sds R41) b = 0 pmf (sds R43) c = 0 pmf (sds R43) b = 0 pmf (sds R44) b = 0 pmf (sds R47) b = 0 (pmf (sds R19) c + pmf (sds R19) a < pmf (sds R10) c + pmf (sds R10) a ∨ pmf (sds R19) c + (pmf (sds R19) a + pmf (sds R19) d) < pmf (sds R10) c + (pmf (sds R10) a + pmf (sds R10) d)) ∨ pmf (sds R19) c + pmf (sds R19) a = pmf (sds R10) c + pmf (sds R10) a ∧ pmf (sds R19) c + (pmf (sds R19) a + pmf (sds R19) d) = pmf (sds R10) c + (pmf (sds R10) a + pmf (sds R10) d) pmf (sds R39) d + pmf (sds R39) c < pmf (sds R36) d + pmf (sds R36) c ∨ pmf (sds R39) d + pmf (sds R39) c = pmf (sds R36) d + pmf (sds R36) c (pmf (sds R10) a < pmf (sds R36) a ∨ pmf (sds R10) a + pmf (sds R10) b < pmf (sds R36) a + pmf (sds R36) b) ∨ pmf (sds R10) a = pmf (sds R36) a ∧ pmf (sds R10) a + pmf (sds R10) b = pmf (sds R36) a + pmf (sds R36) b pmf (sds R1) b + pmf (sds R1) a < pmf (sds R19) b + pmf (sds R19) a ∨ pmf (sds R1) b + pmf (sds R1) a = pmf (sds R19) b + pmf (sds R19) a pmf (sds R27) d + pmf (sds R27) c < pmf (sds R19) d + pmf (sds R19) c ∨ pmf (sds R27) d + pmf (sds R27) c = pmf (sds R19) d + pmf (sds R19) c pmf (sds R13) d + pmf (sds R13) b < pmf (sds R15) d + pmf (sds R15) c ∨ pmf (sds R13) d + pmf (sds R13) b = pmf (sds R15) d + pmf (sds R15) c (pmf (sds R7) d + pmf (sds R7) b < pmf (sds R15) d + pmf (sds R15) b ∨ pmf (sds R7) d + (pmf (sds R7) b + pmf (sds R7) a) < pmf (sds R15) d + (pmf (sds R15) b + pmf (sds R15) a)) ∨ pmf (sds R7) d + pmf (sds R7) b = pmf (sds R15) d + pmf (sds R15) b ∧ pmf (sds R7) d + (pmf (sds R7) b + pmf (sds R7) a) = pmf (sds R15) d + (pmf (sds R15) b + pmf (sds R15) a) (pmf (sds R5) d < pmf (sds R15) a ∨ pmf (sds R5) d + pmf (sds R5) b < pmf (sds R15) a + pmf (sds R15) c ∨ pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) ∨ pmf (sds R5) d = pmf (sds R15) a ∧ pmf (sds R5) d + pmf (sds R5) b = pmf (sds R15) a + pmf (sds R15) c ∧ pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d) pmf (sds R3) c + pmf (sds R3) a < pmf (sds R17) c + pmf (sds R17) a ∨ pmf (sds R3) c + pmf (sds R3) a = pmf (sds R17) c + pmf (sds R17) a pmf (sds R38) c + pmf (sds R38) a < pmf (sds R2) c + pmf (sds R2) a ∨ pmf (sds R38) c + pmf (sds R38) a = pmf (sds R2) c + pmf (sds R2) a (pmf (sds R1) d + pmf (sds R1) c < pmf (sds R2) d + pmf (sds R2) c ∨ pmf (sds R1) d + (pmf (sds R1) c + pmf (sds R1) a) < pmf (sds R2) d + (pmf (sds R2) c + pmf (sds R2) a)) ∨ pmf (sds R1) d + pmf (sds R1) c = pmf (sds R2) d + pmf (sds R2) c ∧ pmf (sds R1) d + (pmf (sds R1) c + pmf (sds R1) a) = pmf (sds R2) d + (pmf (sds R2) c + pmf (sds R2) a) (pmf (sds R15) d + pmf (sds R15) c < pmf (sds R13) d + pmf (sds R13) b ∨ pmf (sds R15) d + (pmf (sds R15) c + pmf (sds R15) a) < pmf (sds R13) d + (pmf (sds R13) b + pmf (sds R13) a)) ∨ pmf (sds R15) d + pmf (sds R15) c = pmf (sds R13) d + pmf (sds R13) b ∧ pmf (sds R15) d + (pmf (sds R15) c + pmf (sds R15) a) = pmf (sds R13) d + (pmf (sds R13) b + pmf (sds R13) a) (pmf (sds R17) c + pmf (sds R17) b < pmf (sds R5) c + pmf (sds R5) a ∨ pmf (sds R17) c + (pmf (sds R17) b + pmf (sds R17) d) < pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)) ∨ pmf (sds R17) c + pmf (sds R17) b = pmf (sds R5) c + pmf (sds R5) a ∧ pmf (sds R17) c + (pmf (sds R17) b + pmf (sds R17) d) = pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d) (pmf (sds R17) c + pmf (sds R17) a < pmf (sds R5) c + pmf (sds R5) a ∨ pmf (sds R17) c + (pmf (sds R17) a + pmf (sds R17) d) < pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)) ∨ pmf (sds R17) c + pmf (sds R17) a = pmf (sds R5) c + pmf (sds R5) a ∧ pmf (sds R17) c + (pmf (sds R17) a + pmf (sds R17) d) = pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d) pmf (sds R2) d + pmf (sds R2) c < pmf (sds R1) d + pmf (sds R1) c ∨ pmf (sds R2) d + pmf (sds R2) c = pmf (sds R1) d + pmf (sds R1) c (pmf (sds R19) a < pmf (sds R1) a ∨ pmf (sds R19) a + pmf (sds R19) b < pmf (sds R1) a + pmf (sds R1) b) ∨ pmf (sds R19) a = pmf (sds R1) a ∧ pmf (sds R19) a + pmf (sds R19) b = pmf (sds R1) a + pmf (sds R1) b (pmf (sds R2) c + pmf (sds R2) a < pmf (sds R39) c + pmf (sds R39) a ∨ pmf (sds R2) c + (pmf (sds R2) a + pmf (sds R2) d) < pmf (sds R39) c + (pmf (sds R39) a + pmf (sds R39) d)) ∨ pmf (sds R2) c + pmf (sds R2) a = pmf (sds R39) c + pmf (sds R39) a ∧ pmf (sds R2) c + (pmf (sds R2) a + pmf (sds R2) d) = pmf (sds R39) c + (pmf (sds R39) a + pmf (sds R39) d) pmf (sds R40) c + pmf (sds R40) d < pmf (sds R44) d + pmf (sds R44) c ∨ pmf (sds R40) c + pmf (sds R40) d = pmf (sds R44) d + pmf (sds R44) c (pmf (sds R12) b + pmf (sds R12) a < pmf (sds R44) b + pmf (sds R44) a ∨ pmf (sds R12) b + (pmf (sds R12) a + pmf (sds R12) d) < pmf (sds R44) b + (pmf (sds R44) a + pmf (sds R44) d)) ∨ pmf (sds R12) b + pmf (sds R12) a = pmf (sds R44) b + pmf (sds R44) a ∧ pmf (sds R12) b + (pmf (sds R12) a + pmf (sds R12) d) = pmf (sds R44) b + (pmf (sds R44) a + pmf (sds R44) d) (pmf (sds R43) d < pmf (sds R7) a ∨ pmf (sds R43) d + pmf (sds R43) b < pmf (sds R7) a + pmf (sds R7) c ∨ pmf (sds R43) d + (pmf (sds R43) b + pmf (sds R43) a) < pmf (sds R7) a + (pmf (sds R7) c + pmf (sds R7) d)) ∨ pmf (sds R43) d = pmf (sds R7) a ∧ pmf (sds R43) d + pmf (sds R43) b = pmf (sds R7) a + pmf (sds R7) c ∧ pmf (sds R43) d + (pmf (sds R43) b + pmf (sds R43) a) = pmf (sds R7) a + (pmf (sds R7) c + pmf (sds R7) d) (pmf (sds R19) d + pmf (sds R19) c < pmf (sds R27) d + pmf (sds R27) b ∨ pmf (sds R19) d + (pmf (sds R19) c + pmf (sds R19) a) < pmf (sds R27) d + (pmf (sds R27) b + pmf (sds R27) a)) ∨ pmf (sds R19) d + pmf (sds R19) c = pmf (sds R27) d + pmf (sds R27) b ∧ pmf (sds R19) d + (pmf (sds R19) c + pmf (sds R19) a) = pmf (sds R27) d + (pmf (sds R27) b + pmf (sds R27) a) pmf (sds R18) c + pmf (sds R18) d < pmf (sds R23) d + pmf (sds R23) c ∨ pmf (sds R18) c + pmf (sds R18) d = pmf (sds R23) d + pmf (sds R23) c pmf (sds R12) c + pmf (sds R12) a < pmf (sds R23) c + pmf (sds R23) a ∨ pmf (sds R12) c + pmf (sds R12) a = pmf (sds R23) c + pmf (sds R23) a pmf (sds R24) b + pmf (sds R24) a < pmf (sds R42) b + pmf (sds R42) a ∨ pmf (sds R24) b + pmf (sds R24) a = pmf (sds R42) b + pmf (sds R42) a (pmf (sds R3) d < pmf (sds R42) d ∨ pmf (sds R3) d + pmf (sds R3) b < pmf (sds R42) d + pmf (sds R42) b ∨ pmf (sds R3) d + (pmf (sds R3) b + pmf (sds R3) a) < pmf (sds R42) d + (pmf (sds R42) b + pmf (sds R42) a)) ∨ pmf (sds R3) d = pmf (sds R42) d ∧ pmf (sds R3) d + pmf (sds R3) b = pmf (sds R42) d + pmf (sds R42) b ∧ pmf (sds R3) d + (pmf (sds R3) b + pmf (sds R3) a) = pmf (sds R42) d + (pmf (sds R42) b + pmf (sds R42) a) pmf (sds R30) b + pmf (sds R30) a < pmf (sds R47) b + pmf (sds R47) a ∨ pmf (sds R30) b + pmf (sds R30) a = pmf (sds R47) b + pmf (sds R47) a pmf (sds R42) c + pmf (sds R42) a < pmf (sds R6) c + pmf (sds R6) a ∨ pmf (sds R42) c + pmf (sds R42) a = pmf (sds R6) c + pmf (sds R6) a (pmf (sds R19) d < pmf (sds R6) d ∨ pmf (sds R19) d + pmf (sds R19) b < pmf (sds R6) d + pmf (sds R6) b ∨ pmf (sds R19) d + (pmf (sds R19) b + pmf (sds R19) a) < pmf (sds R6) d + (pmf (sds R6) b + pmf (sds R6) a)) ∨ pmf (sds R19) d = pmf (sds R6) d ∧ pmf (sds R19) d + pmf (sds R19) b = pmf (sds R6) d + pmf (sds R6) b ∧ pmf (sds R19) d + (pmf (sds R19) b + pmf (sds R19) a) = pmf (sds R6) d + (pmf (sds R6) b + pmf (sds R6) a) (pmf (sds R16) c + pmf (sds R16) a < pmf (sds R12) c + pmf (sds R12) a ∨ pmf (sds R16) c + (pmf (sds R16) a + pmf (sds R16) d) < pmf (sds R12) c + (pmf (sds R12) a + pmf (sds R12) d)) ∨ pmf (sds R16) c + pmf (sds R16) a = pmf (sds R12) c + pmf (sds R12) a ∧ pmf (sds R16) c + (pmf (sds R16) a + pmf (sds R16) d) = pmf (sds R12) c + (pmf (sds R12) a + pmf (sds R12) d) pmf (sds R40) b + pmf (sds R40) a < pmf (sds R9) b + pmf (sds R9) a ∨ pmf (sds R40) b + pmf (sds R40) a = pmf (sds R9) b + pmf (sds R9) a (pmf (sds R18) d + pmf (sds R18) a < pmf (sds R9) d + pmf (sds R9) a ∨ pmf (sds R18) d + (pmf (sds R18) a + pmf (sds R18) c) < pmf (sds R9) d + (pmf (sds R9) a + pmf (sds R9) c)) ∨ pmf (sds R18) d + pmf (sds R18) a = pmf (sds R9) d + pmf (sds R9) a ∧ pmf (sds R18) d + (pmf (sds R18) a + pmf (sds R18) c) = pmf (sds R9) d + (pmf (sds R9) a + pmf (sds R9) c) pmf (sds R22) d + pmf (sds R22) c < pmf (sds R33) d + pmf (sds R33) c ∨ pmf (sds R22) d + pmf (sds R22) c = pmf (sds R33) d + pmf (sds R33) c (pmf (sds R5) a < pmf (sds R33) a ∨ pmf (sds R5) a + pmf (sds R5) b < pmf (sds R33) a + pmf (sds R33) b) ∨ pmf (sds R5) a = pmf (sds R33) a ∧ pmf (sds R5) a + pmf (sds R5) b = pmf (sds R33) a + pmf (sds R33) b (pmf (sds R26) d + pmf (sds R26) c < pmf (sds R25) d + pmf (sds R25) b ∨ pmf (sds R26) d + (pmf (sds R26) c + pmf (sds R26) a) < pmf (sds R25) d + (pmf (sds R25) b + pmf (sds R25) a)) ∨ pmf (sds R26) d + pmf (sds R26) c = pmf (sds R25) d + pmf (sds R25) b ∧ pmf (sds R26) d + (pmf (sds R26) c + pmf (sds R26) a) = pmf (sds R25) d + (pmf (sds R25) b + pmf (sds R25) a) pmf (sds R7) c + pmf (sds R7) a < pmf (sds R17) c + pmf (sds R17) a ∨ pmf (sds R7) c + pmf (sds R7) a = pmf (sds R17) c + pmf (sds R17) a pmf (sds R11) c + pmf (sds R11) a < pmf (sds R17) c + pmf (sds R17) a ∨ pmf (sds R11) c + pmf (sds R11) a = pmf (sds R17) c + pmf (sds R17) a (pmf (sds R21) c < pmf (sds R20) a ∨ pmf (sds R21) c + pmf (sds R21) b < pmf (sds R20) a + pmf (sds R20) c) ∨ pmf (sds R21) c = pmf (sds R20) a ∧ pmf (sds R21) c + pmf (sds R21) b = pmf (sds R20) a + pmf (sds R20) c (pmf (sds R24) c < pmf (sds R34) b ∨ pmf (sds R24) c + (pmf (sds R24) a + pmf (sds R24) d) < pmf (sds R34) b + (pmf (sds R34) d + pmf (sds R34) a)) ∨ pmf (sds R24) c = pmf (sds R34) b ∧ pmf (sds R24) c + (pmf (sds R24) a + pmf (sds R24) d) = pmf (sds R34) b + (pmf (sds R34) d + pmf (sds R34) a) (pmf (sds R10) d < pmf (sds R5) d ∨ pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a) < pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)) ∨ pmf (sds R10) d = pmf (sds R5) d ∧ pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a) = pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) (pmf (sds R38) b + pmf (sds R38) d < pmf (sds R31) d + pmf (sds R31) b ∨ pmf (sds R38) b + (pmf (sds R38) d + pmf (sds R38) c) < pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a)) ∨ pmf (sds R38) b + pmf (sds R38) d = pmf (sds R31) d + pmf (sds R31) b ∧ pmf (sds R38) b + (pmf (sds R38) d + pmf (sds R38) c) = pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a) (pmf (sds R41) c < pmf (sds R30) c ∨ pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) < pmf (sds R30) c + (pmf (sds R30) b + pmf (sds R30) a)) ∨ pmf (sds R41) c = pmf (sds R30) c ∧ pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) = pmf (sds R30) c + (pmf (sds R30) b + pmf (sds R30) a) (pmf (sds R21) b + pmf (sds R21) a < pmf (sds R30) b + pmf (sds R30) a ∨ pmf (sds R21) b + (pmf (sds R21) a + pmf (sds R21) d) < pmf (sds R30) b + (pmf (sds R30) a + pmf (sds R30) d)) ∨ pmf (sds R21) b + pmf (sds R21) a = pmf (sds R30) b + pmf (sds R30) a ∧ pmf (sds R21) b + (pmf (sds R21) a + pmf (sds R21) d) = pmf (sds R30) b + (pmf (sds R30) a + pmf (sds R30) d) (pmf (sds R35) c < pmf (sds R21) c ∨ pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a) < pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a)) ∨ pmf (sds R35) c = pmf (sds R21) c ∧ pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a) = pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a) pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a) < pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) ∨ pmf (sds R31) d + (pmf (sds R31) b + pmf (sds R31) a) = pmf (sds R41) c + (pmf (sds R41) b + pmf (sds R41) a) (pmf (sds R28) a < pmf (sds R32) d ∨ pmf (sds R28) a + (pmf (sds R28) c + pmf (sds R28) d) < pmf (sds R32) d + (pmf (sds R32) b + pmf (sds R32) a)) ∨ pmf (sds R28) a = pmf (sds R32) d ∧ pmf (sds R28) a + (pmf (sds R28) c + pmf (sds R28) d) = pmf (sds R32) d + (pmf (sds R32) b + pmf (sds R32) a) (pmf (sds R22) b + pmf (sds R22) a < pmf (sds R32) b + pmf (sds R32) a ∨ pmf (sds R22) b + (pmf (sds R22) a + pmf (sds R22) d) < pmf (sds R32) b + (pmf (sds R32) a + pmf (sds R32) d)) ∨ pmf (sds R22) b + pmf (sds R22) a = pmf (sds R32) b + pmf (sds R32) a ∧ pmf (sds R22) b + (pmf (sds R22) a + pmf (sds R22) d) = pmf (sds R32) b + (pmf (sds R32) a + pmf (sds R32) d) (pmf (sds R9) a < pmf (sds R35) a ∨ pmf (sds R9) a + pmf (sds R9) b < pmf (sds R35) a + pmf (sds R35) b) ∨ pmf (sds R9) a = pmf (sds R35) a ∧ pmf (sds R9) a + pmf (sds R9) b = pmf (sds R35) a + pmf (sds R35) b (pmf (sds R29) d < pmf (sds R22) d ∨ pmf (sds R29) d + (pmf (sds R29) b + pmf (sds R29) a) < pmf (sds R22) d + (pmf (sds R22) b + pmf (sds R22) a)) ∨ pmf (sds R29) d = pmf (sds R22) d ∧ pmf (sds R29) d + (pmf (sds R29) b + pmf (sds R29) a) = pmf (sds R22) d + (pmf (sds R22) b + pmf (sds R22) a) pmf (sds R19) d + (pmf (sds R19) b + pmf (sds R19) a) < pmf (sds R23) d + (pmf (sds R23) b + pmf (sds R23) a) ∨ pmf (sds R19) d + (pmf (sds R19) b + pmf (sds R19) a) = pmf (sds R23) d + (pmf (sds R23) b + pmf (sds R23) a) (pmf (sds R11) d < pmf (sds R42) c ∨ pmf (sds R11) d + pmf (sds R11) b < pmf (sds R42) c + pmf (sds R42) a) ∨ pmf (sds R11) d = pmf (sds R42) c ∧ pmf (sds R11) d + pmf (sds R11) b = pmf (sds R42) c + pmf (sds R42) a pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) < pmf (sds R12) d + (pmf (sds R12) b + pmf (sds R12) a) ∨ pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) = pmf (sds R12) d + (pmf (sds R12) b + pmf (sds R12) a) (pmf (sds R34) b < pmf (sds R24) c ∨ pmf (sds R34) b + pmf (sds R34) d < pmf (sds R24) c + pmf (sds R24) a) ∨ pmf (sds R34) b = pmf (sds R24) c ∧ pmf (sds R34) b + pmf (sds R34) d = pmf (sds R24) c + pmf (sds R24) a (pmf (sds R36) a < pmf (sds R25) a ∨ pmf (sds R36) a + pmf (sds R36) c < pmf (sds R25) a + pmf (sds R25) c) ∨ pmf (sds R36) a = pmf (sds R25) a ∧ pmf (sds R36) a + pmf (sds R36) c = pmf (sds R25) a + pmf (sds R25) c (pmf (sds R42) d < pmf (sds R37) a ∨ pmf (sds R42) d + pmf (sds R42) b < pmf (sds R37) a + pmf (sds R37) b) ∨ pmf (sds R42) d = pmf (sds R37) a ∧ pmf (sds R42) d + pmf (sds R42) b = pmf (sds R37) a + pmf (sds R37) b (pmf (sds R27) a < pmf (sds R13) a ∨ pmf (sds R27) a + pmf (sds R27) b < pmf (sds R13) a + pmf (sds R13) b ∨ pmf (sds R27) a + (pmf (sds R27) b + pmf (sds R27) d) < pmf (sds R13) a + (pmf (sds R13) b + pmf (sds R13) d)) ∨ pmf (sds R27) a = pmf (sds R13) a ∧ pmf (sds R27) a + pmf (sds R27) b = pmf (sds R13) a + pmf (sds R13) b ∧ pmf (sds R27) a + (pmf (sds R27) b + pmf (sds R27) d) = pmf (sds R13) a + (pmf (sds R13) b + pmf (sds R13) d) pmf (sds R13) b + pmf (sds R13) a < pmf (sds R27) b + pmf (sds R27) a ∨ pmf (sds R13) b + pmf (sds R13) a = pmf (sds R27) b + pmf (sds R27) a (pmf (sds R16) c < pmf (sds R14) d ∨ pmf (sds R16) c + pmf (sds R16) d < pmf (sds R14) d + pmf (sds R14) c) ∨ pmf (sds R16) c = pmf (sds R14) d ∧ pmf (sds R16) c + pmf (sds R16) d = pmf (sds R14) d + pmf (sds R14) c pmf (sds R34) d + (pmf (sds R34) b + pmf (sds R34) a) < pmf (sds R14) c + (pmf (sds R14) b + pmf (sds R14) a) ∨ pmf (sds R34) d + (pmf (sds R34) b + pmf (sds R34) a) = pmf (sds R14) c + (pmf (sds R14) b + pmf (sds R14) a) (pmf (sds R9) a < pmf (sds R14) a ∨ pmf (sds R9) a + pmf (sds R9) d < pmf (sds R14) a + pmf (sds R14) d ∨ pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) < pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)) ∨ pmf (sds R9) a = pmf (sds R14) a ∧ pmf (sds R9) a + pmf (sds R9) d = pmf (sds R14) a + pmf (sds R14) d ∧ pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) = pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c) (pmf (sds R31) c + pmf (sds R31) d < pmf (sds R45) b + pmf (sds R45) a ∨ pmf (sds R31) c + (pmf (sds R31) d + pmf (sds R31) b) < pmf (sds R45) b + (pmf (sds R45) a + pmf (sds R45) c)) ∨ pmf (sds R31) c + pmf (sds R31) d = pmf (sds R45) b + pmf (sds R45) a ∧ pmf (sds R31) c + (pmf (sds R31) d + pmf (sds R31) b) = pmf (sds R45) b + (pmf (sds R45) a + pmf (sds R45) c) (pmf (sds R29) d + pmf (sds R29) c < pmf (sds R39) d + pmf (sds R39) c ∨ pmf (sds R29) d + (pmf (sds R29) c + pmf (sds R29) a) < pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)) ∨ pmf (sds R29) d + pmf (sds R29) c = pmf (sds R39) d + pmf (sds R39) c ∧ pmf (sds R29) d + (pmf (sds R29) c + pmf (sds R29) a) = pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a) (pmf (sds R37) a + pmf (sds R37) c < pmf (sds R46) d + pmf (sds R46) b ∨ pmf (sds R37) a + (pmf (sds R37) c + pmf (sds R37) d) < pmf (sds R46) d + (pmf (sds R46) b + pmf (sds R46) a)) ∨ pmf (sds R37) a + pmf (sds R37) c = pmf (sds R46) d + pmf (sds R46) b ∧ pmf (sds R37) a + (pmf (sds R37) c + pmf (sds R37) d) = pmf (sds R46) d + (pmf (sds R46) b + pmf (sds R46) a) pmf (sds R20) c + pmf (sds R20) a < pmf (sds R46) c + pmf (sds R46) a ∨ pmf (sds R20) c + pmf (sds R20) a = pmf (sds R46) c + pmf (sds R46) a (pmf (sds R26) a < pmf (sds R8) d ∨ pmf (sds R26) a + (pmf (sds R26) c + pmf (sds R26) d) < pmf (sds R8) d + (pmf (sds R8) b + pmf (sds R8) a)) ∨ pmf (sds R26) a = pmf (sds R8) d ∧ pmf (sds R26) a + (pmf (sds R26) c + pmf (sds R26) d) = pmf (sds R8) d + (pmf (sds R8) b + pmf (sds R8) a) (pmf (sds R39) a < pmf (sds R28) a ∨ pmf (sds R39) a + pmf (sds R39) c < pmf (sds R28) a + pmf (sds R28) b) ∨ pmf (sds R39) a = pmf (sds R28) a ∧ pmf (sds R39) a + pmf (sds R39) c = pmf (sds R28) a + pmf (sds R28) b pmf (sds R47) d + pmf (sds R47) a < pmf (sds R4) d + pmf (sds R4) a ∨ pmf (sds R47) d + pmf (sds R47) a = pmf (sds R4) d + pmf (sds R4) a (pmf (sds R18) c < pmf (sds R4) c ∨ pmf (sds R18) c + (pmf (sds R18) b + pmf (sds R18) a) < pmf (sds R4) c + (pmf (sds R4) b + pmf (sds R4) a)) ∨ pmf (sds R18) c = pmf (sds R4) c ∧ pmf (sds R18) c + (pmf (sds R18) b + pmf (sds R18) a) = pmf (sds R4) c + (pmf (sds R4) b + pmf (sds R4) a) (pmf (sds R8) c < pmf (sds R4) d ∨ pmf (sds R8) c + pmf (sds R8) d < pmf (sds R4) d + pmf (sds R4) c) ∨ pmf (sds R8) c = pmf (sds R4) d ∧ pmf (sds R8) c + pmf (sds R8) d = pmf (sds R4) d + pmf (sds R4) c goal (1 subgoal): 1. False