Anne is big. Anne is kind. Anne is nice. Anne is not quiet. Anne is white. Gary is kind. Gary is not nice. Rough, kind things are not quiet. If Anne is nice and Anne is white then Anne is rough. If something is rough and not quiet then it is cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is white.
("Anne" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Rough, kind things are not quiet.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "-"))
If Anne is nice and Anne is white then Anne is rough.
((("Anne" "is" "nice" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "rough" "+"))
If something is rough and not quiet then it is cold.
((("something" "is" "rough" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "cold" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is quiet.
False
1
inv-proof
[(triple4 OR ((((triple3 triple5) -> rule2) triple2) -> rule1))]
("Anne" "is" "quiet" "+")
triple4
((((triple3 triple5) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is rough.
True
3
proof
[(((triple3 triple5) -> rule2))]
("Anne" "is" "rough" "+")
((triple3 triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
3
inv-proof
[(((triple3 triple5) -> rule2))]
("Anne" "is" "rough" "-")
((triple3 triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
True
5
proof
[(((((triple3 triple5) -> rule2) triple4) -> rule3) OR ((((triple3 triple5) -> rule2) ((((triple3 triple5) -> rule2) triple2) -> rule1)) -> rule3))]
("Anne" "is" "cold" "+")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((((triple3 triple5) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((((triple3 triple5) -> rule2) triple4) -> rule3) OR ((((triple3 triple5) -> rule2) ((((triple3 triple5) -> rule2) triple2) -> rule1)) -> rule3))]
("Anne" "is" "cold" "-")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((((triple3 triple5) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is not quiet.[(triple4 OR ((((triple3 triple5) -> rule2) triple2) -> rule1))] Anne is white.[(triple5)] Gary is kind.[(triple6)] Gary is not nice.[(triple7)] @1: Anne is rough.[(((triple3 triple5) -> rule2))] @2: Anne is cold.[(((((triple3 triple5) -> rule2) triple4) -> rule3) OR ((((triple3 triple5) -> rule2) ((((triple3 triple5) -> rule2) triple2) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
((((triple3 triple5) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is not nice.
("Gary" "is" "nice" "-")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple3 triple5) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((((triple3 triple5) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3