Bob is nice. Gary is rough. If Gary is rough then Gary is blue. If Bob is white and Bob is nice then Bob is rough.
Bob is nice.
("Bob" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is rough then Gary is blue.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "blue" "+"))
If Bob is white and Bob is nice then Bob is rough.
((("Bob" "is" "white" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple2)]
("Gary" "is" "rough" "+")
triple2
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Gary is blue.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Gary is rough.[(triple2)] @1: Gary is blue.[(((triple2) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1