Anne is blue. Anne is white. Charlie is nice. Charlie is white. Gary is kind. Gary is nice. Gary is quiet. If someone is white and not nice then they are not green. All cold, nice people are not green. If someone is green then they are white. Nice people are white. If Anne is cold then Anne is white. If someone is kind and white then they are not cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is white and not nice then they are not green.
((("someone" "is" "white" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "-"))
All cold, nice people are not green.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "-"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Anne is cold then Anne is white.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "white" "+"))
If someone is kind and white then they are not cold.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "-"))
Charlie is white.
True
1
proof
[(triple4 OR ((triple3) -> rule4))]
("Charlie" "is" "white" "+")
triple4
((triple3) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Gary is white.
True
2
proof
[(((triple6) -> rule4))]
("Gary" "is" "white" "+")
((triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple6) -> rule4))]
("Gary" "is" "white" "-")
((triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not cold.
True
4
proof
[(((triple5 ((triple6) -> rule4)) -> rule6))]
("Gary" "is" "cold" "-")
((triple5 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
False
4
inv-proof
[(((triple5 ((triple6) -> rule4)) -> rule6))]
("Gary" "is" "cold" "+")
((triple5 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is white.[(triple2)] Charlie is nice.[(triple3)] Charlie is white.[(triple4 OR ((triple3) -> rule4))] Gary is kind.[(triple5)] Gary is nice.[(triple6)] Gary is quiet.[(triple7)] @1: Gary is white.[(((triple6) -> rule4))] @2: Gary is not cold.[(((triple5 ((triple6) -> rule4)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((triple3) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
((triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
((triple5 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2