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