The cat is round. All rough things are kind. If the cat is blue then the cat is rough. If something is cold then it is blue. If something is rough and round then it is blue. If something is rough and blue then it is kind. If something is cold and round then it is blue.
The cat is round.
("cat" "is" "round" "+")
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If the cat is blue then the cat is rough.
((("cat" "is" "blue" "+")) -> ("cat" "is" "rough" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is rough and round then it is blue.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is rough and blue then it is kind.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is cold and round then it is blue.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
The cat is round.
True
1
proof
[(triple1)]
("cat" "is" "round" "+")
triple1
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The cat is not blue.
Unknown
inv-rconc
[@3: The cat is blue.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule3 <- FAIL)]]
("cat" "is" "blue" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is round.[(triple1)]
The cat is round.
("cat" "is" "round" "+")
triple1