Anne is nice. Gary is red. Gary is smart. All white, furry people are red. If Gary is red and Gary is smart then Gary is round. Furry people are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All white, furry people are red.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If Gary is red and Gary is smart then Gary is round.
((("Gary" "is" "red" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "round" "+"))
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple3)]
("Gary" "is" "smart" "+")
triple3
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Gary is round.
True
3
proof
[(((triple2 triple3) -> rule2))]
("Gary" "is" "round" "+")
((triple2 triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("Gary" "is" "round" "-")
((triple2 triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "red" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Gary is red.[(triple2)] Gary is smart.[(triple3)] @1: Gary is round.[(((triple2 triple3) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
((triple2 triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1