Anne is rough. Dave is big. Gary is quiet. If someone is quiet and big then they are round. All furry people are rough. All rough, furry people are big. All round, furry people are white. All rough people are cold. All round, quiet people are cold.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is quiet and big then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
All rough, furry people are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All round, furry people are white.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All round, quiet people are cold.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is rough.[(triple1)] Dave is big.[(triple2)] Gary is quiet.[(triple3)] @1: Anne is cold.[(((triple1) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1