Anne is big. Anne is round. Dave is furry. Dave is nice. Dave is not quiet. Dave is smart. Harry is big. If something is furry then it is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple7)]
("Harry" "is" "big" "+")
triple7
Dave is not nice.
False
1
inv-proof
[(triple4)]
("Dave" "is" "nice" "-")
triple4
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is big.[(triple1)] Anne is round.[(triple2)] Dave is furry.[(triple3)] Dave is nice.[(triple4)] Dave is not quiet.[(triple5)] Dave is smart.[(triple6)] Harry is big.[(triple7)] @1: Dave is big.[(((triple3) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1