Anne is kind. If Anne is rough then Anne is not nice. If Anne is not smart then Anne is red. If Anne is kind then Anne is rough. If Anne is smart and Anne is nice then Anne is big. If someone is cold and not nice then they are big. All rough people are big.
Anne is kind.
("Anne" "is" "kind" "+")
If Anne is rough then Anne is not nice.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "nice" "-"))
If Anne is not smart then Anne is red.
((("Anne" "is" "smart" "~")) -> ("Anne" "is" "red" "+"))
If Anne is kind then Anne is rough.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "rough" "+"))
If Anne is smart and Anne is nice then Anne is big.
((("Anne" "is" "smart" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
If someone is cold and not nice then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "big" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Anne is rough.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] @1: Anne is rough.[(((triple1) -> rule3))] @2: Anne is big.[(((((triple1) -> rule3)) -> rule6))] Anne is not nice.[(((((triple1) -> rule3)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2