Charlie is cold. Dave is white. Gary is red. All big people are not rough. If someone is rough then they are red. Cold, rough people are big. If Charlie is not red then Charlie is not smart. Smart people are quiet. All red people are quiet.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
All big people are not rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Cold, rough people are big.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Charlie is not red then Charlie is not smart.
((("Charlie" "is" "red" "~")) -> ("Charlie" "is" "smart" "-"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Dave is white.[(triple2)] Gary is red.[(triple3)] @1: Gary is quiet.[(((triple3) -> rule6))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1