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