The cat is rough. If the cat is rough and the cat is young then the cat is kind. If someone is young and big then they are nice. All nice people are rough. All kind, young people are big. If someone is kind then they are young. If the cat is big then the cat is rough.
The cat is rough.
("cat" "is" "rough" "+")
If the cat is rough and the cat is young then the cat is kind.
((("cat" "is" "rough" "+") ("cat" "is" "young" "+")) -> ("cat" "is" "kind" "+"))
If someone is young and big then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All kind, young people are big.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If the cat is big then the cat is rough.
((("cat" "is" "big" "+")) -> ("cat" "is" "rough" "+"))
The cat is rough.
True
1
proof
[(triple1)]
("cat" "is" "rough" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cat is not nice.
Unknown
inv-rconc
[@3: The cat is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("cat" "is" "nice" "-")
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 rough.[(triple1)]
The cat is rough.
("cat" "is" "rough" "+")
triple1