The bear sees the lion. The cow is rough. The dog is round. The lion chases the dog. The lion eats the cow. The lion is red. The lion is rough. If someone is nice and they see the bear then they chase the bear. If someone is red then they eat the bear. If the lion chases the dog then the lion chases the cow. If someone chases the dog and they see the dog then the dog is round. If someone sees the lion and they see the dog then the dog chases the cow. If someone eats the bear and the bear chases the lion then the bear eats the lion.
The bear sees the lion.
("bear" "sees" "lion" "+")
The cow is rough.
("cow" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
If someone is nice and they see the bear then they chase the bear.
((("someone" "is" "nice" "+") ("someone" "sees" "bear" "+")) -> ("someone" "chases" "bear" "+"))
If someone is red then they eat the bear.
((("someone" "is" "red" "+")) -> ("someone" "eats" "bear" "+"))
If the lion chases the dog then the lion chases the cow.
((("lion" "chases" "dog" "+")) -> ("lion" "chases" "cow" "+"))
If someone chases the dog and they see the dog then the dog is round.
((("someone" "chases" "dog" "+") ("someone" "sees" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone sees the lion and they see the dog then the dog chases the cow.
((("someone" "sees" "lion" "+") ("someone" "sees" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If someone eats the bear and the bear chases the lion then the bear eats the lion.
((("someone" "eats" "bear" "+") ("bear" "chases" "lion" "+")) -> ("bear" "eats" "lion" "+"))
The bear sees the lion.
True
1
proof
[(triple1)]
("bear" "sees" "lion" "+")
triple1
The lion does not eat the cow.
False
1
inv-proof
[(triple5)]
("lion" "eats" "cow" "-")
triple5
The bear does not eat the lion.
Unknown
inv-rconc
[@1: The bear eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "lion" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The bear sees the lion.[(triple1)] The cow is rough.[(triple2)] The dog is round.[(triple3)] The lion chases the dog.[(triple4)] The lion eats the cow.[(triple5)] The lion is red.[(triple6)] The lion is rough.[(triple7)] @1: The lion chases the cow.[(((triple4) -> rule3))] The lion eats the bear.[(((triple6) -> rule2))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The lion chases the dog.
("lion" "chases" "dog" "+")
triple4
The lion eats the cow.
("lion" "eats" "cow" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple7
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple4) -> (rule3 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple6) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1