Anne is big. Anne is blue. Anne is cold. Anne is red. Anne is smart. Bob is blue. Bob is cold. Bob is quiet. Bob is red. Bob is round. Bob is smart. Dave is blue. Dave is red. Dave is round. Harry is red. Harry is round. All red things are quiet. If Harry is round then Harry is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Harry is round then Harry is smart.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "smart" "+"))
Harry is red.
True
1
proof
[(triple15)]
("Harry" "is" "red" "+")
triple15
Dave is not blue.
False
1
inv-proof
[(triple12)]
("Dave" "is" "blue" "-")
triple12
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
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 blue.[(triple2)] Anne is cold.[(triple3)] Anne is red.[(triple4)] Anne is smart.[(triple5)] Bob is blue.[(triple6)] Bob is cold.[(triple7)] Bob is quiet.[(triple8 OR ((triple9) -> rule1))] Bob is red.[(triple9)] Bob is round.[(triple10)] Bob is smart.[(triple11)] Dave is blue.[(triple12)] Dave is red.[(triple13)] Dave is round.[(triple14)] Harry is red.[(triple15)] Harry is round.[(triple16)] @1: Anne is quiet.[(((triple4) -> rule1))] Dave is quiet.[(((triple13) -> rule1))] Harry is quiet.[(((triple15) -> rule1))] Harry is smart.[(((triple16) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
((triple9) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple9
Bob is round.
("Bob" "is" "round" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
triple11
Dave is blue.
("Dave" "is" "blue" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple13) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple15) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1