Anne is big. Anne is furry. Anne is rough. Anne is smart. Anne is young. Bob is kind. Bob is smart. Bob is young. Dave is rough. Dave is young. If something is big then it is round. All rough, kind things are furry.
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 young.
("Anne" "is" "young" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All rough, kind things are furry.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Dave is rough.
True
1
proof
[(triple9)]
("Dave" "is" "rough" "+")
triple9
Anne is not furry.
False
1
inv-proof
[(triple2)]
("Anne" "is" "furry" "-")
triple2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
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 furry.[(triple2)] Anne is rough.[(triple3)] Anne is smart.[(triple4)] Anne is young.[(triple5)] Bob is kind.[(triple6)] Bob is smart.[(triple7)] Bob is young.[(triple8)] Dave is rough.[(triple9)] Dave is young.[(triple10)] @1: Anne is round.[(((triple1) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1