The cat is big. The cow needs the cat. If the cow is kind and the cow is round then the cow likes the cat. If something eats the cat and the cat likes the cow then the cow likes the cat. If something eats the cat then the cat is big.
The cat is big.
("cat" "is" "big" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
If the cow is kind and the cow is round then the cow likes the cat.
((("cow" "is" "kind" "+") ("cow" "is" "round" "+")) -> ("cow" "likes" "cat" "+"))
If something eats the cat and the cat likes the cow then the cow likes the cat.
((("something" "eats" "cat" "+") ("cat" "likes" "cow" "+")) -> ("cow" "likes" "cat" "+"))
If something eats the cat then the cat is big.
((("something" "eats" "cat" "+")) -> ("cat" "is" "big" "+"))
The cow needs the cat.
True
1
proof
[(triple2)]
("cow" "needs" "cat" "+")
triple2
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cat" "-")
The cat eats the cow.
Unknown
random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "+")
@0: The cat is big.[(triple1)] The cow needs the cat.[(triple2)]
The cat is big.
("cat" "is" "big" "+")
triple1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple2