Bob is blue. All furry, big things are rough. If something is furry and blue then it is kind. If something is big then it is furry. If Bob is blue and Bob is kind then Bob is big. All young, cold things are big. All rough, blue things are young. If something is young and kind then it is rough. If something is furry then it is big.
Bob is blue.
("Bob" "is" "blue" "+")
All furry, big things are rough.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is furry and blue then it is kind.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Bob is blue and Bob is kind then Bob is big.
((("Bob" "is" "blue" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "big" "+"))
All young, cold things are big.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All rough, blue things are young.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is young and kind then it is rough.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is not rough.
Unknown
inv-rconc
[@4: Bob is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule4 <- rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is blue.[(triple1)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1