Erin is round. All round things are smart. All big, round things are smart. If something is young and round then it is big. All red, white things are cold. Cold things are smart. All round, white things are red.
Erin is round.
("Erin" "is" "round" "+")
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All big, round things are smart.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is young and round then it is big.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All red, white things are cold.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All round, white things are red.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Erin is round.
True
1
proof
[(triple1)]
("Erin" "is" "round" "+")
triple1
Erin is not round.
False
1
inv-proof
[(triple1)]
("Erin" "is" "round" "-")
triple1
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Erin is round.[(triple1)] @1: Erin is smart.[(((triple1) -> rule1))]
Erin is round.
("Erin" "is" "round" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1