Anne is big. Anne is cold. Anne is quiet. Anne is red. Anne is white. Anne is young. Bob is big. Bob is cold. Bob is red. Bob is rough. Bob is white. Bob is young. White people are cold. If someone is young then they are white. If Bob is white and Bob is rough then Bob is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Bob is white and Bob is rough then Bob is red.
((("Bob" "is" "white" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "red" "+"))
Anne is cold.
True
1
proof
[(triple2 OR ((triple5) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Anne" "is" "cold" "+")
triple2
((triple5) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not white.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule2))]
("Anne" "is" "white" "-")
triple5
((triple6) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple5) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is white.[(triple5 OR ((triple6) -> rule2))] Anne is young.[(triple6)] Bob is big.[(triple7)] Bob is cold.[(triple8 OR ((triple11) -> rule1) OR ((((triple12) -> rule2)) -> rule1))] Bob is red.[(triple9 OR ((triple11 triple10) -> rule3) OR ((((triple12) -> rule2) triple10) -> rule3))] Bob is rough.[(triple10)] Bob is white.[(triple11 OR ((triple12) -> rule2))] Bob is young.[(triple12)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple5) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple6) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple6
Bob is big.
("Bob" "is" "big" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
triple8
((triple11) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple9
((triple11 triple10) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple12) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple10
Bob is white.
("Bob" "is" "white" "+")
triple11
((triple12) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple12