Bob is green. Bob is not red. Dave is not furry. Dave is red. Gary is green. Gary is not young. Harry is green. All red, blue people are white. All blue people are nice. All green people are not young. If Dave is green then Dave is blue. If Dave is young and Dave is nice then Dave is white. If Gary is red and Gary is not furry then Gary is not young.
Bob is green.
("Bob" "is" "green" "+")
Bob is not red.
("Bob" "is" "red" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is red.
("Dave" "is" "red" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is green.
("Harry" "is" "green" "+")
All red, blue people are white.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
All green people are not young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "-"))
If Dave is green then Dave is blue.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "blue" "+"))
If Dave is young and Dave is nice then Dave is white.
((("Dave" "is" "young" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "white" "+"))
If Gary is red and Gary is not furry then Gary is not young.
((("Gary" "is" "red" "+") ("Gary" "is" "furry" "~")) -> ("Gary" "is" "young" "-"))
Gary is not young.
True
1
proof
[(triple6 OR ((triple5) -> rule3))]
("Gary" "is" "young" "-")
triple6
((triple5) -> (rule3 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Bob is not young.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "young" "-")
((triple1) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Harry is young.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "young" "+")
((triple7) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "nice" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is green.[(triple1)] Bob is not red.[(triple2)] Dave is not furry.[(triple3)] Dave is red.[(triple4)] Gary is green.[(triple5)] Gary is not young.[(triple6 OR ((triple5) -> rule3))] Harry is green.[(triple7)] @1: Bob is not young.[(((triple1) -> rule3))] Harry is not young.[(((triple7) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not red.
("Bob" "is" "red" "-")
triple2
Dave is not furry.
("Dave" "is" "furry" "-")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is not young.
("Gary" "is" "young" "-")
triple6
((triple5) -> (rule3 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
triple7
Bob is not young.
("Bob" "is" "young" "-")
((triple1) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Harry is not young.
("Harry" "is" "young" "-")
((triple7) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1