Charlie is smart. If something is rough and not red then it is furry. All rough, big things are not furry. Smart things are rough.
Charlie is smart.
("Charlie" "is" "smart" "+")
If something is rough and not red then it is furry.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "furry" "+"))
All rough, big things are not furry.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "-"))
Smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is smart.[(triple1)] @1: Charlie is rough.[(((triple1) -> rule3))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1