ea9009727600ed1500ddf3adca7794017422c33eKarl Luc(and (P a) (P b))
6e37a8341c202773dc9db886547b7018ee834d3bTill Mossakowski(not (P a)) %implied
6e37a8341c202773dc9db886547b7018ee834d3bTill Mossakowski(and (P a) (not (P a))) %(contra)% %implied
ea9009727600ed1500ddf3adca7794017422c33eKarl Luc(Cube a) %(one)%
ea9009727600ed1500ddf3adca7794017422c33eKarl Luc(Dodec b) %(two)%
ea9009727600ed1500ddf3adca7794017422c33eKarl Luc(or (Cube a) (Cube b)) %implied
ea9009727600ed1500ddf3adca7794017422c33eKarl Luc(and (P b) (P c))
ea9009727600ed1500ddf3adca7794017422c33eKarl Luc(and (P a) (P c)) %(transitivity)% %implied