Dave is blue. Dave is red. Gary is cold. Gary is kind. Gary is smart. Harry is blue. Harry is smart. If something is cold and smart then it is blue. All kind things are red.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is cold and smart then it is blue.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Gary is kind.
True
1
proof
[(triple4)]
("Gary" "is" "kind" "+")
triple4
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "red" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Dave is blue.[(triple1)] Dave is red.[(triple2)] Gary is cold.[(triple3)] Gary is kind.[(triple4)] Gary is smart.[(triple5)] Harry is blue.[(triple6)] Harry is smart.[(triple7)] @1: Gary is blue.[(((triple3 triple5) -> rule1))] Gary is red.[(((triple4) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple3 triple5) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1