The bear is green. The bear likes the dog. The bear likes the rabbit. The bear sees the rabbit. The dog is not blue. The dog visits the bear. The rabbit is blue. The rabbit likes the dog. The rabbit visits the bear. The rabbit does not visit the dog. If something sees the dog and it is not nice then it visits the rabbit. If something likes the dog and the dog visits the bear then the bear visits the dog. If something visits the dog then the dog does not visit the rabbit.
The bear is green.
("bear" "is" "green" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The dog is not blue.
("dog" "is" "blue" "-")
The dog visits the bear.
("dog" "visits" "bear" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
If something sees the dog and it is not nice then it visits the rabbit.
((("something" "sees" "dog" "+") ("something" "is" "nice" "~")) -> ("something" "visits" "rabbit" "+"))
If something likes the dog and the dog visits the bear then the bear visits the dog.
((("something" "likes" "dog" "+") ("dog" "visits" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If something visits the dog then the dog does not visit the rabbit.
((("something" "visits" "dog" "+")) -> ("dog" "visits" "rabbit" "-"))
The bear likes the dog.
True
1
proof
[(triple2)]
("bear" "likes" "dog" "+")
triple2
The bear does not like the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "likes" "rabbit" "-")
triple3
The bear visits the dog.
True
3
proof
[(((triple2 triple6) -> rule2) OR ((triple8 triple6) -> rule2))]
("bear" "visits" "dog" "+")
((triple2 triple6) -> (rule2 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
((triple8 triple6) -> (rule2 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear does not visit the dog.
False
3
inv-proof
[(((triple2 triple6) -> rule2) OR ((triple8 triple6) -> rule2))]
("bear" "visits" "dog" "-")
((triple2 triple6) -> (rule2 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
((triple8 triple6) -> (rule2 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog does not visit the rabbit.
True
4
proof
[(((((triple2 triple6) -> rule2)) -> rule3) OR ((((triple8 triple6) -> rule2)) -> rule3))]
("dog" "visits" "rabbit" "-")
((((triple2 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
((((triple8 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog visits the rabbit.
False
4
inv-proof
[(((((triple2 triple6) -> rule2)) -> rule3) OR ((((triple8 triple6) -> rule2)) -> rule3))]
("dog" "visits" "rabbit" "+")
((((triple2 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
((((triple8 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The bear visits the rabbit.
Unknown
rconc
[@1: The bear visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "rabbit" "+")
The rabbit does not see the bear.
Unknown
inv-random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
The dog does not like the rabbit.
Unknown
inv-random
[@0: The dog likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "rabbit" "-")
The rabbit likes the bear.
Unknown
random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "+")
@0: The bear is green.[(triple1)] The bear likes the dog.[(triple2)] The bear likes the rabbit.[(triple3)] The bear sees the rabbit.[(triple4)] The dog is not blue.[(triple5)] The dog visits the bear.[(triple6)] The rabbit does not visit the dog.[(triple10)] The rabbit is blue.[(triple7)] The rabbit likes the dog.[(triple8)] The rabbit visits the bear.[(triple9)] @1: The bear visits the dog.[(((triple2 triple6) -> rule2) OR ((triple8 triple6) -> rule2))] @2: The dog does not visit the rabbit.[(((((triple2 triple6) -> rule2)) -> rule3) OR ((((triple8 triple6) -> rule2)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear likes the dog.
("bear" "likes" "dog" "+")
triple2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The dog is not blue.
("dog" "is" "blue" "-")
triple5
The dog visits the bear.
("dog" "visits" "bear" "+")
triple6
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple8
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple9
The bear visits the dog.
("bear" "visits" "dog" "+")
((triple2 triple6) -> (rule2 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
((triple8 triple6) -> (rule2 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
((((triple2 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
((((triple8 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2