Bob is cold. Bob is rough. Gary is green. If someone is cold and smart then they are rough. If Gary is green then Gary is smart. All big people are smart. Blue people are rough. Smart, white people are blue. All blue people are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is green.
("Gary" "is" "green" "+")
If someone is cold and smart then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Gary is green then Gary is smart.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "smart" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Smart, white people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is cold.[(triple1)] Bob is rough.[(triple2)] Gary is green.[(triple3)] @1: Gary is smart.[(((triple3) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1