The bear chases the lion. The bear does not eat the lion. The dog eats the bear. The dog is not round. The dog visits the lion. The lion chases the bear. The lion eats the bear. The lion does not eat the dog. The lion eats the rabbit. The lion is kind. The lion is round. The lion visits the dog. The rabbit eats the dog. The rabbit eats the lion. The rabbit visits the dog. The rabbit visits the lion. If someone eats the dog then they visit the rabbit. If someone visits the lion then the lion does not chase the rabbit. If someone eats the lion then the lion eats the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear does not eat the lion.
("bear" "eats" "lion" "-")
The dog eats the bear.
("dog" "eats" "bear" "+")
The dog is not round.
("dog" "is" "round" "-")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion does not eat the dog.
("lion" "eats" "dog" "-")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone eats the dog then they visit the rabbit.
((("someone" "eats" "dog" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the lion then the lion does not chase the rabbit.
((("someone" "visits" "lion" "+")) -> ("lion" "chases" "rabbit" "-"))
If someone eats the lion then the lion eats the bear.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "bear" "+"))
The lion visits the dog.
True
1
proof
[(triple12)]
("lion" "visits" "dog" "+")
triple12
The lion does not eat the rabbit.
False
1
inv-proof
[(triple9)]
("lion" "eats" "rabbit" "-")
triple9
The rabbit visits the rabbit.
True
2
proof
[(((triple13) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((triple13) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple13) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((triple13) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The dog does not visit the rabbit.
Unknown
inv-rconc
[@1: The dog visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "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 dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
@0: The bear chases the lion.[(triple1)] The bear does not eat the lion.[(triple2)] The dog eats the bear.[(triple3)] The dog is not round.[(triple4)] The dog visits the lion.[(triple5)] The lion chases the bear.[(triple6)] The lion does not eat the dog.[(triple8)] The lion eats the bear.[(triple7 OR ((triple14) -> rule3))] The lion eats the rabbit.[(triple9)] The lion is kind.[(triple10)] The lion is round.[(triple11)] The lion visits the dog.[(triple12)] The rabbit eats the dog.[(triple13)] The rabbit eats the lion.[(triple14)] The rabbit visits the dog.[(triple15)] The rabbit visits the lion.[(triple16)] @1: The lion does not chase the rabbit.[(((triple16) -> rule2) OR ((triple5) -> rule2))] The rabbit visits the rabbit.[(((triple13) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear does not eat the lion.
("bear" "eats" "lion" "-")
triple2
The dog eats the bear.
("dog" "eats" "bear" "+")
triple3
The dog is not round.
("dog" "is" "round" "-")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple5
The lion chases the bear.
("lion" "chases" "bear" "+")
triple6
The lion does not eat the dog.
("lion" "eats" "dog" "-")
triple8
The lion eats the bear.
("lion" "eats" "bear" "+")
triple7
((triple14) -> (rule3 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple9
The lion is kind.
("lion" "is" "kind" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
triple11
The lion visits the dog.
("lion" "visits" "dog" "+")
triple12
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple13
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple14
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple15
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple16
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
((triple16) -> (rule2 % int1))
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
int1
((triple5) -> (rule2 % int1))
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple13) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1