The bear chases the dog. The bear chases the squirrel. The cat chases the bear. The cat chases the dog. The cat is rough. The cat does not like the dog. The dog does not chase the bear. The dog is cold. The squirrel is red. The squirrel likes the cat. The squirrel needs the cat. The squirrel needs the dog. If something likes the cat and it is young then it does not need the cat. If something is big then it does not need the cat. If something needs the dog then the dog likes the cat. If something likes the cat then the cat is red. If the squirrel is cold and the squirrel does not chase the dog then the squirrel is red. If something likes the dog then it likes the bear.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat does not like the dog.
("cat" "likes" "dog" "-")
The dog does not chase the bear.
("dog" "chases" "bear" "-")
The dog is cold.
("dog" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something likes the cat and it is young then it does not need the cat.
((("something" "likes" "cat" "+") ("something" "is" "young" "+")) -> ("something" "needs" "cat" "-"))
If something is big then it does not need the cat.
((("something" "is" "big" "+")) -> ("something" "needs" "cat" "-"))
If something needs the dog then the dog likes the cat.
((("something" "needs" "dog" "+")) -> ("dog" "likes" "cat" "+"))
If something likes the cat then the cat is red.
((("something" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
If the squirrel is cold and the squirrel does not chase the dog then the squirrel is red.
((("squirrel" "is" "cold" "+") ("squirrel" "chases" "dog" "~")) -> ("squirrel" "is" "red" "+"))
If something likes the dog then it likes the bear.
((("something" "likes" "dog" "+")) -> ("something" "likes" "bear" "+"))
The cat is rough.
True
1
proof
[(triple5)]
("cat" "is" "rough" "+")
triple5
The squirrel does not like the cat.
False
1
inv-proof
[(triple10)]
("squirrel" "likes" "cat" "-")
triple10
The dog likes the cat.
True
2
proof
[(((triple12) -> rule3))]
("dog" "likes" "cat" "+")
((triple12) -> (rule3 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple10) -> rule4) OR ((((triple12) -> rule3)) -> rule4))]
("cat" "is" "red" "-")
((triple10) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "bear" "-")
The dog likes the bear.
Unknown
rconc
[@1: The dog likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "bear" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The squirrel chases the dog.
Unknown
random
[@0: The squirrel chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "dog" "+")
@0: The bear chases the dog.[(triple1)] The bear chases the squirrel.[(triple2)] The cat chases the bear.[(triple3)] The cat chases the dog.[(triple4)] The cat does not like the dog.[(triple6)] The cat is rough.[(triple5)] The dog does not chase the bear.[(triple7)] The dog is cold.[(triple8)] The squirrel is red.[(triple9)] The squirrel likes the cat.[(triple10)] The squirrel needs the cat.[(triple11)] The squirrel needs the dog.[(triple12)] @1: The cat is red.[(((triple10) -> rule4) OR ((((triple12) -> rule3)) -> rule4))] The dog likes the cat.[(((triple12) -> rule3))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple3
The cat chases the dog.
("cat" "chases" "dog" "+")
triple4
The cat does not like the dog.
("cat" "likes" "dog" "-")
triple6
The cat is rough.
("cat" "is" "rough" "+")
triple5
The dog does not chase the bear.
("dog" "chases" "bear" "-")
triple7
The dog is cold.
("dog" "is" "cold" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple10
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple11
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple12
The cat is red.
("cat" "is" "red" "+")
((triple10) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The dog likes the cat.
("dog" "likes" "cat" "+")
((triple12) -> (rule3 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1