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