Charlie is red. Dave is kind. Gary is blue. Kind, nice people are cold. All quiet people are cold. If someone is quiet and cold then they are not blue. All nice, red people are blue. All red people are green. If someone is nice and not kind then they are red. Kind people are red. If Gary is quiet then Gary is blue.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Kind, nice people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and cold then they are not blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "-"))
All nice, red people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and not kind then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Gary is quiet then Gary is blue.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "blue" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Dave is red.
True
2
proof
[(((triple2) -> rule7))]
("Dave" "is" "red" "+")
((triple2) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "green" "-")
((triple1) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Gary is green.
Unknown
rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Gary" "is" "green" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is red.[(triple1)] Dave is kind.[(triple2)] Gary is blue.[(triple3)] @1: Charlie is green.[(((triple1) -> rule5))] Dave is red.[(((triple2) -> rule7))] @2: Dave is green.[(((((triple2) -> rule7)) -> rule5))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2