Bob is blue. Bob is not cold. Bob is not smart. If someone is round and not rough then they are cold. All round, smart people are cold. All smart, round people are quiet. All quiet people are round. Smart people are not round. All rough people are not blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
If someone is round and not rough then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "cold" "+"))
All round, smart people are cold.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All smart, round people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Smart people are not round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "-"))
All rough people are not blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
Bob is not smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "-")
triple3
Bob is smart.
False
1
inv-proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is blue.[(triple1)] Bob is not cold.[(triple2)] Bob is not smart.[(triple3)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is not smart.
("Bob" "is" "smart" "-")
triple3