The bear is red. The bear needs the rabbit. The bear visits the cat. The cat needs the cow. The cat needs the rabbit. The cat sees the cow. The cat visits the cow. The cow is kind. The cow needs the bear. The cow needs the cat. The cow needs the rabbit. The cow sees the rabbit. The rabbit does not need the cat. The rabbit needs the cow. The rabbit visits the cat. If something visits the cat and it needs the rabbit then it visits the rabbit. If something needs the bear then the bear visits the cat.
The bear is red.
("bear" "is" "red" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something visits the cat and it needs the rabbit then it visits the rabbit.
((("something" "visits" "cat" "+") ("something" "needs" "rabbit" "+")) -> ("something" "visits" "rabbit" "+"))
If something needs the bear then the bear visits the cat.
((("something" "needs" "bear" "+")) -> ("bear" "visits" "cat" "+"))
The rabbit visits the cat.
True
1
proof
[(triple15)]
("rabbit" "visits" "cat" "+")
triple15
The cow does not need the bear.
False
1
inv-proof
[(triple9)]
("cow" "needs" "bear" "-")
triple9
The bear visits the rabbit.
True
3
proof
[(((triple3 triple2) -> rule1) OR ((((triple9) -> rule2) triple2) -> rule1))]
("bear" "visits" "rabbit" "+")
((triple3 triple2) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
((((triple9) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear does not visit the rabbit.
False
3
inv-proof
[(((triple3 triple2) -> rule1) OR ((((triple9) -> rule2) triple2) -> rule1))]
("bear" "visits" "rabbit" "-")
((triple3 triple2) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
((((triple9) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
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 cow visits the rabbit.
Unknown
rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "rabbit" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cat visits the bear.
Unknown
random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "+")
@0: The bear is red.[(triple1)] The bear needs the rabbit.[(triple2)] The bear visits the cat.[(triple3 OR ((triple9) -> rule2))] The cat needs the cow.[(triple4)] The cat needs the rabbit.[(triple5)] The cat sees the cow.[(triple6)] The cat visits the cow.[(triple7)] The cow is kind.[(triple8)] The cow needs the bear.[(triple9)] The cow needs the cat.[(triple10)] The cow needs the rabbit.[(triple11)] The cow sees the rabbit.[(triple12)] The rabbit does not need the cat.[(triple13)] The rabbit needs the cow.[(triple14)] The rabbit visits the cat.[(triple15)] @1: The bear visits the rabbit.[(((triple3 triple2) -> rule1) OR ((((triple9) -> rule2) triple2) -> rule1))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
((triple9) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple4
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple5
The cat sees the cow.
("cat" "sees" "cow" "+")
triple6
The cat visits the cow.
("cat" "visits" "cow" "+")
triple7
The cow is kind.
("cow" "is" "kind" "+")
triple8
The cow needs the bear.
("cow" "needs" "bear" "+")
triple9
The cow needs the cat.
("cow" "needs" "cat" "+")
triple10
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple11
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple12
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
triple13
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple14
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
((triple3 triple2) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
((((triple9) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2