Bob is blue. Bob is quiet. Bob is smart. All quiet, young people are blue. If Bob is quiet then Bob is furry. Big, young people are red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All quiet, young people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If Bob is quiet then Bob is furry.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "furry" "+"))
Big, young people are red.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Bob is smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is furry.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is quiet.[(triple2)] Bob is smart.[(triple3)] @1: Bob is furry.[(((triple2) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1