The bear chases the dog. The bear is big. The bear needs the dog. The cat chases the bear. The cat chases the dog. The cat visits the dog. The dog is blue. The dog is rough. The dog needs the bear. The dog visits the cat. If something needs the bear and the bear needs the dog then the bear needs the cat. If the cat is green then the cat chases the dog. If something is big and rough then it visits the dog.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is big.
("bear" "is" "big" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If something needs the bear and the bear needs the dog then the bear needs the cat.
((("something" "needs" "bear" "+") ("bear" "needs" "dog" "+")) -> ("bear" "needs" "cat" "+"))
If the cat is green then the cat chases the dog.
((("cat" "is" "green" "+")) -> ("cat" "chases" "dog" "+"))
If something is big and rough then it visits the dog.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "visits" "dog" "+"))
The cat chases the bear.
True
1
proof
[(triple4)]
("cat" "chases" "bear" "+")
triple4
The cat does not chase the dog.
False
1
inv-proof
[(triple5)]
("cat" "chases" "dog" "-")
triple5
The bear needs the cat.
True
3
proof
[(((triple9 triple3) -> rule1))]
("bear" "needs" "cat" "+")
((triple9 triple3) -> (rule1 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear does not need the cat.
False
3
inv-proof
[(((triple9 triple3) -> rule1))]
("bear" "needs" "cat" "-")
((triple9 triple3) -> (rule1 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear does not visit the dog.
Unknown
inv-rconc
[@1: The bear visits the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "dog" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "dog" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The bear chases the dog.[(triple1)] The bear is big.[(triple2)] The bear needs the dog.[(triple3)] The cat chases the bear.[(triple4)] The cat chases the dog.[(triple5)] The cat visits the dog.[(triple6)] The dog is blue.[(triple7)] The dog is rough.[(triple8)] The dog needs the bear.[(triple9)] The dog visits the cat.[(triple10)] @1: The bear needs the cat.[(((triple9 triple3) -> rule1))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
The cat chases the dog.
("cat" "chases" "dog" "+")
triple5
The cat visits the dog.
("cat" "visits" "dog" "+")
triple6
The dog is blue.
("dog" "is" "blue" "+")
triple7
The dog is rough.
("dog" "is" "rough" "+")
triple8
The dog needs the bear.
("dog" "needs" "bear" "+")
triple9
The dog visits the cat.
("dog" "visits" "cat" "+")
triple10
The bear needs the cat.
("bear" "needs" "cat" "+")
((triple9 triple3) -> (rule1 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1