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