Anne is big. Anne is smart. Dave is round. Dave is smart. Gary is big. Gary is furry. Gary is green. Rough, round people are green. Big, red people are furry. All furry people are red. If Anne is green and Anne is smart then Anne is red. Green, smart people are red. If someone is round then they are smart. If Dave is big then Dave is smart. All rough, big people are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Rough, round people are green.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Big, red people are furry.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If Anne is green and Anne is smart then Anne is red.
((("Anne" "is" "green" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "red" "+"))
Green, smart people are red.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If Dave is big then Dave is smart.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "smart" "+"))
All rough, big people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Dave is not smart.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule6))]
("Dave" "is" "smart" "-")
triple4
((triple3) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is red.
True
2
proof
[(((triple6) -> rule3))]
("Gary" "is" "red" "+")
((triple6) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple6) -> rule3))]
("Gary" "is" "red" "-")
((triple6) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is not furry.
Unknown
inv-rconc
[@3: Anne is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule8 <- FAIL)]]
("Anne" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is smart.[(triple2)] Dave is round.[(triple3)] Dave is smart.[(triple4 OR ((triple3) -> rule6))] Gary is big.[(triple5)] Gary is furry.[(triple6)] Gary is green.[(triple7)] @1: Gary is red.[(((triple6) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((triple3) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
((triple6) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1