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