Anne is big. Anne is furry. Anne is green. Anne is quiet. Anne is white. Harry is big. Harry is furry. Harry is green. Harry is quiet. Harry is smart. Harry is white. Harry is young. Quiet, white things are furry. If Harry is young then Harry is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Quiet, white things are furry.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Harry is young then Harry is smart.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "smart" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple10 OR ((triple12) -> rule2))]
("Harry" "is" "smart" "-")
triple10
((triple12) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple4 triple5) -> rule1))] Anne is green.[(triple3)] Anne is quiet.[(triple4)] Anne is white.[(triple5)] Harry is big.[(triple6)] Harry is furry.[(triple7 OR ((triple9 triple11) -> rule1))] Harry is green.[(triple8)] Harry is quiet.[(triple9)] Harry is smart.[(triple10 OR ((triple12) -> rule2))] Harry is white.[(triple11)] Harry is young.[(triple12)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4 triple5) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
((triple9 triple11) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple12) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12