The cat likes the squirrel. The cat likes the tiger. The rabbit chases the cat. The rabbit is big. The rabbit is red. The rabbit likes the cat. The rabbit likes the tiger. The squirrel is big. The squirrel likes the cat. The tiger chases the cat. The tiger is big. The tiger needs the rabbit. If something likes the squirrel and it needs the rabbit then it likes the tiger. If something chases the squirrel then the squirrel is red. If something is cold then it chases the squirrel. If something is blue and nice then it is big. If something chases the cat and the cat is nice then it chases the tiger. If the rabbit is red and the rabbit needs the squirrel then the squirrel chases the tiger.
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something likes the squirrel and it needs the rabbit then it likes the tiger.
((("something" "likes" "squirrel" "+") ("something" "needs" "rabbit" "+")) -> ("something" "likes" "tiger" "+"))
If something chases the squirrel then the squirrel is red.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something is cold then it chases the squirrel.
((("something" "is" "cold" "+")) -> ("something" "chases" "squirrel" "+"))
If something is blue and nice then it is big.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something chases the cat and the cat is nice then it chases the tiger.
((("something" "chases" "cat" "+") ("cat" "is" "nice" "+")) -> ("something" "chases" "tiger" "+"))
If the rabbit is red and the rabbit needs the squirrel then the squirrel chases the tiger.
((("rabbit" "is" "red" "+") ("rabbit" "needs" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
The squirrel likes the cat.
True
1
proof
[(triple9)]
("squirrel" "likes" "cat" "+")
triple9
The rabbit is not big.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "big" "-")
triple4
The cat does not chase the squirrel.
Unknown
inv-rconc
[@1: The cat chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "squirrel" "-")
The squirrel needs the cat.
Unknown
random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "+")
@0: The cat likes the squirrel.[(triple1)] The cat likes the tiger.[(triple2)] The rabbit chases the cat.[(triple3)] The rabbit is big.[(triple4)] The rabbit is red.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit likes the tiger.[(triple7)] The squirrel is big.[(triple8)] The squirrel likes the cat.[(triple9)] The tiger chases the cat.[(triple10)] The tiger is big.[(triple11)] The tiger needs the rabbit.[(triple12)]
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple12