Anne is big. Anne is furry. Anne is rough. Anne is smart. Anne is white. Charlie is green. Charlie is white. Dave is big. Dave is furry. Gary is rough. Gary is smart. Gary is white. All big, furry people are rough. If Gary is smart then Gary is white.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All big, furry people are rough.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Gary is smart then Gary is white.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "white" "+"))
Anne is smart.
True
1
proof
[(triple4)]
("Anne" "is" "smart" "+")
triple4
Anne is not rough.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule1))]
("Anne" "is" "rough" "-")
triple3
((triple1 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is rough.
True
3
proof
[(((triple8 triple9) -> rule1))]
("Dave" "is" "rough" "+")
((triple8 triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
3
inv-proof
[(((triple8 triple9) -> rule1))]
("Dave" "is" "rough" "-")
((triple8 triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is rough.[(triple3 OR ((triple1 triple2) -> rule1))] Anne is smart.[(triple4)] Anne is white.[(triple5)] Charlie is green.[(triple6)] Charlie is white.[(triple7)] Dave is big.[(triple8)] Dave is furry.[(triple9)] Gary is rough.[(triple10)] Gary is smart.[(triple11)] Gary is white.[(triple12 OR ((triple11) -> rule2))] @1: Dave is rough.[(((triple8 triple9) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple1 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
((triple11) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple8 triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1