Charlie is green. Gary is not green. If someone is big then they are green. Green, quiet people are smart. If Gary is quiet then Gary is not nice. All smart, big people are quiet. All smart people are cold. If Charlie is quiet then Charlie is cold.
Charlie is green.
("Charlie" "is" "green" "+")
Gary is not green.
("Gary" "is" "green" "-")
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Green, quiet people are smart.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Gary is quiet then Gary is not nice.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "-"))
All smart, big people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is quiet then Charlie is cold.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "cold" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Gary is green.
False
1
inv-proof
[(triple2)]
("Gary" "is" "green" "+")
triple2
Gary is not cold.
Unknown
inv-rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is green.[(triple1)] Gary is not green.[(triple2)]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Gary is not green.
("Gary" "is" "green" "-")
triple2