Anne is not big. Anne is kind. Bob is kind. Bob is nice. Charlie is red. Erin is not cold. Erin is not nice. Big things are red. If something is nice then it is not red. If Anne is kind then Anne is nice.
Anne is not big.
("Anne" "is" "big" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not nice.
("Erin" "is" "nice" "-")
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is not red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "-"))
If Anne is kind then Anne is nice.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "nice" "+"))
Erin is not cold.
True
1
proof
[(triple6)]
("Erin" "is" "cold" "-")
triple6
Erin is cold.
False
1
inv-proof
[(triple6)]
("Erin" "is" "cold" "+")
triple6
Bob is not red.
True
2
proof
[(((triple4) -> rule2))]
("Bob" "is" "red" "-")
((triple4) -> (rule2 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Anne is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not red.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Anne" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Anne" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is kind.[(triple2)] Anne is not big.[(triple1)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Charlie is red.[(triple5)] Erin is not cold.[(triple6)] Erin is not nice.[(triple7)] @1: Anne is nice.[(((triple2) -> rule3))] Bob is not red.[(((triple4) -> rule2))] @2: Anne is not red.[(((((triple2) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Erin is not cold.
("Erin" "is" "cold" "-")
triple6
Erin is not nice.
("Erin" "is" "nice" "-")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is not red.
("Bob" "is" "red" "-")
((triple4) -> (rule2 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Anne is not red.
("Anne" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2