Bob is red. Dave is furry. Gary is red. White things are round. Round, smart things are white. Furry things are red. If Bob is red and Bob is white then Bob is round. All smart, kind things are furry. If something is smart then it is furry.
Bob is red.
("Bob" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Round, smart things are white.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Bob is red and Bob is white then Bob is round.
((("Bob" "is" "red" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "round" "+"))
All smart, kind things are furry.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Gary is red.
True
1
proof
[(triple3)]
("Gary" "is" "red" "+")
triple3
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Dave is red.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "red" "+")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "red" "-")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "furry" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is red.[(triple1)] Dave is furry.[(triple2)] Gary is red.[(triple3)] @1: Dave is red.[(((triple2) -> rule3))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1