The cat chases the dog. The cat chases the squirrel. The cat is rough. The cat sees the dog. The cat sees the squirrel. The cat visits the dog. The cat visits the squirrel. The dog is blue. The dog visits the cat. The dog visits the squirrel. The squirrel is rough. The squirrel visits the dog. If someone visits the squirrel then the squirrel visits the dog. If someone is round and they see the dog then they see the cat. If someone chases the cat then they are red. If someone sees the cat then they are red. If someone is red and they see the dog then the dog is round. If someone chases the cat and the cat visits the squirrel then they chase the dog.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone visits the squirrel then the squirrel visits the dog.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If someone is round and they see the dog then they see the cat.
((("someone" "is" "round" "+") ("someone" "sees" "dog" "+")) -> ("someone" "sees" "cat" "+"))
If someone chases the cat then they are red.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "red" "+"))
If someone sees the cat then they are red.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "red" "+"))
If someone is red and they see the dog then the dog is round.
((("someone" "is" "red" "+") ("someone" "sees" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone chases the cat and the cat visits the squirrel then they chase the dog.
((("someone" "chases" "cat" "+") ("cat" "visits" "squirrel" "+")) -> ("someone" "chases" "dog" "+"))
The dog visits the cat.
True
1
proof
[(triple9)]
("dog" "visits" "cat" "+")
triple9
The cat does not see the dog.
False
1
inv-proof
[(triple4)]
("cat" "sees" "dog" "-")
triple4
The squirrel does not chase the dog.
Unknown
inv-rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "chases" "dog" "-")
The dog sees the squirrel.
Unknown
random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "+")
@0: The cat chases the dog.[(triple1)] The cat chases the squirrel.[(triple2)] The cat is rough.[(triple3)] The cat sees the dog.[(triple4)] The cat sees the squirrel.[(triple5)] The cat visits the dog.[(triple6)] The cat visits the squirrel.[(triple7)] The dog is blue.[(triple8)] The dog visits the cat.[(triple9)] The dog visits the squirrel.[(triple10)] The squirrel is rough.[(triple11)] The squirrel visits the dog.[(triple12 OR ((triple10) -> rule1) OR ((triple7) -> rule1))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple5
The cat visits the dog.
("cat" "visits" "dog" "+")
triple6
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple7
The dog is blue.
("dog" "is" "blue" "+")
triple8
The dog visits the cat.
("dog" "visits" "cat" "+")
triple9
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple12
((triple10) -> (rule1 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
((triple7) -> (rule1 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1