Dave is furry. Dave is not red. Dave is white. Gary is furry. Gary is green. Gary is kind. Gary is red. Gary is round. Gary is smart. Gary is white. All red things are green. All round things are red. If something is green and not furry then it is not red.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is green and not furry then it is not red.
((("something" "is" "green" "+") ("something" "is" "furry" "~")) -> ("something" "is" "red" "-"))
Gary is furry.
True
1
proof
[(triple4)]
("Gary" "is" "furry" "+")
triple4
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is furry.[(triple1)] Dave is not red.[(triple2)] Dave is white.[(triple3)] Gary is furry.[(triple4)] Gary is green.[(triple5 OR ((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Gary is kind.[(triple6)] Gary is red.[(triple7 OR ((triple8) -> rule2))] Gary is round.[(triple8)] Gary is smart.[(triple9)] Gary is white.[(triple10)]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is not red.
("Dave" "is" "red" "-")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
((triple7) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
((triple8) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10