The cat does not chase the dog. The cat is nice. The cat visits the dog. The cow chases the cat. The cow is round. The cow visits the dog. The dog is green. The dog is nice. The dog does not visit the cat. The tiger chases the dog. The tiger is big. The tiger is green. If someone is green then they visit the dog. If someone is round then they need the dog. If someone visits the cow and the cow is green then the cow visits the tiger. If someone chases the cat and they do not chase the cow then the cow is green. If someone visits the tiger and they do not chase the dog then they are not big. If someone is green and they do not need the dog then the dog needs the tiger. If someone needs the cat and they are kind then they visit the tiger. If someone needs the cat and the cat does not visit the dog then the dog needs the cat.
The cat does not chase the dog.
("cat" "chases" "dog" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog does not visit the cat.
("dog" "visits" "cat" "-")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone is green then they visit the dog.
((("someone" "is" "green" "+")) -> ("someone" "visits" "dog" "+"))
If someone is round then they need the dog.
((("someone" "is" "round" "+")) -> ("someone" "needs" "dog" "+"))
If someone visits the cow and the cow is green then the cow visits the tiger.
((("someone" "visits" "cow" "+") ("cow" "is" "green" "+")) -> ("cow" "visits" "tiger" "+"))
If someone chases the cat and they do not chase the cow then the cow is green.
((("someone" "chases" "cat" "+") ("someone" "chases" "cow" "~")) -> ("cow" "is" "green" "+"))
If someone visits the tiger and they do not chase the dog then they are not big.
((("someone" "visits" "tiger" "+") ("someone" "chases" "dog" "~")) -> ("someone" "is" "big" "-"))
If someone is green and they do not need the dog then the dog needs the tiger.
((("someone" "is" "green" "+") ("someone" "needs" "dog" "~")) -> ("dog" "needs" "tiger" "+"))
If someone needs the cat and they are kind then they visit the tiger.
((("someone" "needs" "cat" "+") ("someone" "is" "kind" "+")) -> ("someone" "visits" "tiger" "+"))
If someone needs the cat and the cat does not visit the dog then the dog needs the cat.
((("someone" "needs" "cat" "+") ("cat" "visits" "dog" "~")) -> ("dog" "needs" "cat" "+"))
The tiger chases the dog.
True
1
proof
[(triple10)]
("tiger" "chases" "dog" "+")
triple10
The cat chases the dog.
False
1
inv-proof
[(triple1)]
("cat" "chases" "dog" "+")
triple1
The tiger visits the dog.
True
2
proof
[(((triple12) -> rule1))]
("tiger" "visits" "dog" "+")
((triple12) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cow does not need the dog.
False
2
inv-proof
[(((triple5) -> rule2))]
("cow" "needs" "dog" "-")
((triple5) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "visits" "tiger" "-")
The dog needs the tiger.
Unknown
rconc
[@1: The dog needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "tiger" "+")
The tiger does not chase the cow.
Unknown
inv-random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
@0: The cat does not chase the dog.[(triple1)] The cat is nice.[(triple2)] The cat visits the dog.[(triple3)] The cow chases the cat.[(triple4)] The cow is round.[(triple5)] The cow visits the dog.[(triple6)] The dog does not visit the cat.[(triple9)] The dog is green.[(triple7)] The dog is nice.[(triple8)] The tiger chases the dog.[(triple10)] The tiger is big.[(triple11)] The tiger is green.[(triple12)] @1: The cow needs the dog.[(((triple5) -> rule2))] The dog visits the dog.[(((triple7) -> rule1))] The tiger visits the dog.[(((triple12) -> rule1))]
The cat does not chase the dog.
("cat" "chases" "dog" "-")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat visits the dog.
("cat" "visits" "dog" "+")
triple3
The cow chases the cat.
("cow" "chases" "cat" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow visits the dog.
("cow" "visits" "dog" "+")
triple6
The dog does not visit the cat.
("dog" "visits" "cat" "-")
triple9
The dog is green.
("dog" "is" "green" "+")
triple7
The dog is nice.
("dog" "is" "nice" "+")
triple8
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The cow needs the dog.
("cow" "needs" "dog" "+")
((triple5) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple7) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple12) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1