Charlie is green. All furry, young things are quiet. If Charlie is quiet then Charlie is rough. Quiet, smart things are young. All young, furry things are rough. All young, round things are quiet. If Charlie is quiet and Charlie is round then Charlie is smart.
Charlie is green.
("Charlie" "is" "green" "+")
All furry, young things are quiet.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is quiet then Charlie is rough.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "rough" "+"))
Quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All young, furry things are rough.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All young, round things are quiet.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is quiet and Charlie is round then Charlie is smart.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "smart" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is green.[(triple1)]
Charlie is green.
("Charlie" "is" "green" "+")
triple1