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