Dave is green. Gary is furry. Gary is smart. Red, smart people are furry. All white, red people are green. White, smart people are furry. If someone is smart and furry then they are green. All green, furry people are white. All quiet, white people are furry.
Dave is green.
("Dave" "is" "green" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Red, smart people are furry.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All white, red people are green.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
White, smart people are furry.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and furry then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All green, furry people are white.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All quiet, white people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Gary is green.
True
3
proof
[(((triple3 triple2) -> rule4))]
("Gary" "is" "green" "+")
((triple3 triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
3
inv-proof
[(((triple3 triple2) -> rule4))]
("Gary" "is" "green" "-")
((triple3 triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
True
5
proof
[(((((triple3 triple2) -> rule4) triple2) -> rule5))]
("Gary" "is" "white" "+")
((((triple3 triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not white.
False
5
inv-proof
[(((((triple3 triple2) -> rule4) triple2) -> rule5))]
("Gary" "is" "white" "-")
((((triple3 triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Dave is green.[(triple1)] Gary is furry.[(triple2)] Gary is smart.[(triple3)] @1: Gary is green.[(((triple3 triple2) -> rule4))] @2: Gary is white.[(((((triple3 triple2) -> rule4) triple2) -> rule5))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple3 triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple3 triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2