The cat chases the tiger. The cat is not kind. The cat is rough. The cat is round. The cat likes the squirrel. The cat needs the tiger. The rabbit chases the cat. The rabbit is red. The rabbit does not like the squirrel. The rabbit needs the cat. The rabbit needs the squirrel. The squirrel is red. The tiger chases the rabbit. The tiger is not round. The tiger likes the cat. If someone needs the squirrel then they need the cat. If someone likes the squirrel then the squirrel chases the rabbit. If someone likes the rabbit and the rabbit is not red then the rabbit needs the squirrel.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit does not like the squirrel.
("rabbit" "likes" "squirrel" "-")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is not round.
("tiger" "is" "round" "-")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If someone needs the squirrel then they need the cat.
((("someone" "needs" "squirrel" "+")) -> ("someone" "needs" "cat" "+"))
If someone likes the squirrel then the squirrel chases the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "chases" "rabbit" "+"))
If someone likes the rabbit and the rabbit is not red then the rabbit needs the squirrel.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "red" "~")) -> ("rabbit" "needs" "squirrel" "+"))
The rabbit needs the cat.
True
1
proof
[(triple10 OR ((triple11) -> rule1))]
("rabbit" "needs" "cat" "+")
triple10
((triple11) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The tiger is round.
False
1
inv-proof
[(triple14)]
("tiger" "is" "round" "+")
triple14
The tiger does not need the cat.
Unknown
inv-rconc
[@1: The tiger needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "cat" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The cat chases the tiger.[(triple1)] The cat is not kind.[(triple2)] The cat is rough.[(triple3)] The cat is round.[(triple4)] The cat likes the squirrel.[(triple5)] The cat needs the tiger.[(triple6)] The rabbit chases the cat.[(triple7)] The rabbit does not like the squirrel.[(triple9)] The rabbit is red.[(triple8)] The rabbit needs the cat.[(triple10 OR ((triple11) -> rule1))] The rabbit needs the squirrel.[(triple11)] The squirrel is red.[(triple12)] The tiger chases the rabbit.[(triple13)] The tiger is not round.[(triple14)] The tiger likes the cat.[(triple15)] @1: The squirrel chases the rabbit.[(((triple5) -> rule2))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is not kind.
("cat" "is" "kind" "-")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple6
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple7
The rabbit does not like the squirrel.
("rabbit" "likes" "squirrel" "-")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple10
((triple11) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple11
The squirrel is red.
("squirrel" "is" "red" "+")
triple12
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple13
The tiger is not round.
("tiger" "is" "round" "-")
triple14
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple15
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
((triple5) -> (rule2 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1