Charlie is round. All smart, cold people are furry. If someone is young and furry then they are red. Cold, smart people are red. White people are round. If Charlie is smart then Charlie is white. White, smart people are young.
Charlie is round.
("Charlie" "is" "round" "+")
All smart, cold people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is young and furry then they are red.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Cold, smart people are red.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Charlie is smart then Charlie is white.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "white" "+"))
White, smart people are young.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Charlie is not round.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "round" "-")
triple1
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is round.[(triple1)]
Charlie is round.
("Charlie" "is" "round" "+")
triple1