The cow is round. The cow sees the lion. The dog eats the lion. The dog is kind. The dog visits the lion. The lion visits the cow. The lion visits the dog. If someone sees the lion then the lion does not see the cow. If someone visits the lion and the lion is not kind then the lion sees the dog. If someone visits the dog and they see the lion then the lion does not see the dog. If the lion eats the dog then the lion visits the dog. If someone is cold and they see the dog then they do not eat the cow. If the dog eats the cow then the cow is not cold.
The cow is round.
("cow" "is" "round" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone sees the lion then the lion does not see the cow.
((("someone" "sees" "lion" "+")) -> ("lion" "sees" "cow" "-"))
If someone visits the lion and the lion is not kind then the lion sees the dog.
((("someone" "visits" "lion" "+") ("lion" "is" "kind" "~")) -> ("lion" "sees" "dog" "+"))
If someone visits the dog and they see the lion then the lion does not see the dog.
((("someone" "visits" "dog" "+") ("someone" "sees" "lion" "+")) -> ("lion" "sees" "dog" "-"))
If the lion eats the dog then the lion visits the dog.
((("lion" "eats" "dog" "+")) -> ("lion" "visits" "dog" "+"))
If someone is cold and they see the dog then they do not eat the cow.
((("someone" "is" "cold" "+") ("someone" "sees" "dog" "+")) -> ("someone" "eats" "cow" "-"))
If the dog eats the cow then the cow is not cold.
((("dog" "eats" "cow" "+")) -> ("cow" "is" "cold" "-"))
The dog visits the lion.
True
1
proof
[(triple5)]
("dog" "visits" "lion" "+")
triple5
The dog does not visit the lion.
False
1
inv-proof
[(triple5)]
("dog" "visits" "lion" "-")
triple5
The lion does not see the dog.
Unknown
inv-rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "dog" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The cow is round.[(triple1)] The cow sees the lion.[(triple2)] The dog eats the lion.[(triple3)] The dog is kind.[(triple4)] The dog visits the lion.[(triple5)] The lion visits the cow.[(triple6)] The lion visits the dog.[(triple7)] @1: The lion does not see the cow.[(((triple2) -> rule1))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The dog eats the lion.
("dog" "eats" "lion" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple5
The lion visits the cow.
("lion" "visits" "cow" "+")
triple6
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The lion does not see the cow.
("lion" "sees" "cow" "-")
((triple2) -> (rule1 % int1))
The lion does not see the cow.
("lion" "sees" "cow" "-")
int1