Anne is big. Anne is furry. Anne is nice. Anne is red. Anne is round. Anne is smart. Bob is big. Bob is furry. Bob is round. Bob is white. Dave is big. Dave is furry. Dave is round. Dave is smart. Dave is white. Harry is white. White things are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
White things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Bob is round.
True
1
proof
[(triple9)]
("Bob" "is" "round" "+")
triple9
Dave is not smart.
False
1
inv-proof
[(triple14)]
("Dave" "is" "smart" "-")
triple14
Harry is furry.
True
2
proof
[(((triple16) -> rule1))]
("Harry" "is" "furry" "+")
((triple16) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple16) -> rule1))]
("Harry" "is" "furry" "-")
((triple16) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6)] Bob is big.[(triple7)] Bob is furry.[(triple8 OR ((triple10) -> rule1))] Bob is round.[(triple9)] Bob is white.[(triple10)] Dave is big.[(triple11)] Dave is furry.[(triple12 OR ((triple15) -> rule1))] Dave is round.[(triple13)] Dave is smart.[(triple14)] Dave is white.[(triple15)] Harry is white.[(triple16)] @1: Harry is furry.[(((triple16) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Bob is big.
("Bob" "is" "big" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
triple8
((triple10) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple9
Bob is white.
("Bob" "is" "white" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
((triple15) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple13
Dave is smart.
("Dave" "is" "smart" "+")
triple14
Dave is white.
("Dave" "is" "white" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Harry is furry.
("Harry" "is" "furry" "+")
((triple16) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1