Anne is blue. Anne is cold. Anne is nice. Anne is not quiet. Anne is not round. Anne is white. Anne is not young. Gary is blue. Gary is quiet. Gary is young. Round, blue people are not nice. White people are nice. Young, quiet people are cold. If someone is nice and not blue then they are young. If someone is nice and not quiet then they are not young. If Gary is round and Gary is not quiet then Gary is nice. If Gary is cold then Gary is not white. If Anne is blue and Anne is quiet then Anne is not white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is not round.
("Anne" "is" "round" "-")
Anne is white.
("Anne" "is" "white" "+")
Anne is not young.
("Anne" "is" "young" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Round, blue people are not nice.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Young, quiet people are cold.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and not blue then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "+"))
If someone is nice and not quiet then they are not young.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "young" "-"))
If Gary is round and Gary is not quiet then Gary is nice.
((("Gary" "is" "round" "+") ("Gary" "is" "quiet" "~")) -> ("Gary" "is" "nice" "+"))
If Gary is cold then Gary is not white.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "white" "-"))
If Anne is blue and Anne is quiet then Anne is not white.
((("Anne" "is" "blue" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "white" "-"))
Anne is white.
True
1
proof
[(triple6)]
("Anne" "is" "white" "+")
triple6
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Gary is cold.
True
3
proof
[(((triple10 triple9) -> rule3))]
("Gary" "is" "cold" "+")
((triple10 triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
3
inv-proof
[(((triple10 triple9) -> rule3))]
("Gary" "is" "cold" "-")
((triple10 triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not white.
True
4
proof
[(((((triple10 triple9) -> rule3)) -> rule7))]
("Gary" "is" "white" "-")
((((triple10 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
False
4
inv-proof
[(((((triple10 triple9) -> rule3)) -> rule7))]
("Gary" "is" "white" "+")
((((triple10 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is nice.[(triple3 OR ((triple6) -> rule2))] Anne is not quiet.[(triple4)] Anne is not round.[(triple5)] Anne is not young.[(triple7 OR ((triple3 triple4) -> rule5) OR ((((triple6) -> rule2) triple4) -> rule5))] Anne is white.[(triple6)] Gary is blue.[(triple8)] Gary is quiet.[(triple9)] Gary is young.[(triple10)] @1: Gary is cold.[(((triple10 triple9) -> rule3))] @2: Gary is not white.[(((((triple10 triple9) -> rule3)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple6) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
Anne is not round.
("Anne" "is" "round" "-")
triple5
Anne is not young.
("Anne" "is" "young" "-")
triple7
((triple3 triple4) -> (rule5 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
((((triple6) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
((triple10 triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
((((triple10 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2