Charlie is blue. Charlie is furry. Charlie is rough. Charlie is young. Gary is furry. Gary is smart. Gary is young. If Gary is red then Gary is furry. If something is smart and furry then it is red.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is red then Gary is furry.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "furry" "+"))
If something is smart and furry then it is red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Gary is furry.
True
1
proof
[(triple5)]
("Gary" "is" "furry" "+")
triple5
Gary is not furry.
False
1
inv-proof
[(triple5)]
("Gary" "is" "furry" "-")
triple5
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is rough.[(triple3)] Charlie is young.[(triple4)] Gary is furry.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7)] @1: Gary is red.[(((triple6 triple5) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
((triple6 triple5) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1