Bob is red. Gary is quiet. If Bob is red then Bob is not furry. If Bob is red and Bob is nice then Bob is cold. If Bob is nice and Bob is smart then Bob is cold. If someone is quiet and furry then they are cold. All nice people are furry. If someone is nice and not blue then they are smart.
Bob is red.
("Bob" "is" "red" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Bob is red then Bob is not furry.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "furry" "-"))
If Bob is red and Bob is nice then Bob is cold.
((("Bob" "is" "red" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "cold" "+"))
If Bob is nice and Bob is smart then Bob is cold.
((("Bob" "is" "nice" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "cold" "+"))
If someone is quiet and furry then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is nice and not blue then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "smart" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Gary is not quiet.
False
1
inv-proof
[(triple2)]
("Gary" "is" "quiet" "-")
triple2
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is red.[(triple1)] Gary is quiet.[(triple2)] @1: Bob is not furry.[(((triple1) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Bob is not furry.
("Bob" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1