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