The dog is rough. The rabbit needs the dog. The tiger needs the dog. If the rabbit is round then the rabbit does not need the dog. If something is cold and it chases the dog then it is blue. If something is rough then it needs the tiger. If something is young then it needs the tiger. If something chases the rabbit then the rabbit chases the tiger. If something visits the rabbit and the rabbit is round then it is not rough. If the tiger needs the dog and the dog does not visit the tiger then the tiger needs the rabbit. If something chases the dog and the dog is blue then the dog visits the rabbit.
The dog is rough.
("dog" "is" "rough" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If the rabbit is round then the rabbit does not need the dog.
((("rabbit" "is" "round" "+")) -> ("rabbit" "needs" "dog" "-"))
If something is cold and it chases the dog then it is blue.
((("something" "is" "cold" "+") ("something" "chases" "dog" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it needs the tiger.
((("something" "is" "rough" "+")) -> ("something" "needs" "tiger" "+"))
If something is young then it needs the tiger.
((("something" "is" "young" "+")) -> ("something" "needs" "tiger" "+"))
If something chases the rabbit then the rabbit chases the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something visits the rabbit and the rabbit is round then it is not rough.
((("something" "visits" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("something" "is" "rough" "-"))
If the tiger needs the dog and the dog does not visit the tiger then the tiger needs the rabbit.
((("tiger" "needs" "dog" "+") ("dog" "visits" "tiger" "~")) -> ("tiger" "needs" "rabbit" "+"))
If something chases the dog and the dog is blue then the dog visits the rabbit.
((("something" "chases" "dog" "+") ("dog" "is" "blue" "+")) -> ("dog" "visits" "rabbit" "+"))
The rabbit needs the dog.
True
1
proof
[(triple2)]
("rabbit" "needs" "dog" "+")
triple2
The rabbit does not need the dog.
False
1
inv-proof
[(triple2)]
("rabbit" "needs" "dog" "-")
triple2
The dog needs the tiger.
True
2
proof
[(((triple1) -> rule3))]
("dog" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("dog" "needs" "tiger" "-")
((triple1) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "blue" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog chases the rabbit.
Unknown
random
[@0: The dog chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "rabbit" "+")
@0: The dog is rough.[(triple1)] The rabbit needs the dog.[(triple2)] The tiger needs the dog.[(triple3)] @1: The dog needs the tiger.[(((triple1) -> rule3))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1