The bear eats the dog. The cat is not round. The dog sees the cat. If someone is green and they eat the bear then they are nice. If someone is green then they eat the cat. If someone sees the cat then they chase the dog. If someone chases the cat and they do not eat the dog then the cat chases the dog. If someone sees the cat and they are round then they eat the bear. If someone eats the cat and they do not chase the dog then the cat is big.
The bear eats the dog.
("bear" "eats" "dog" "+")
The cat is not round.
("cat" "is" "round" "-")
The dog sees the cat.
("dog" "sees" "cat" "+")
If someone is green and they eat the bear then they are nice.
((("someone" "is" "green" "+") ("someone" "eats" "bear" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they eat the cat.
((("someone" "is" "green" "+")) -> ("someone" "eats" "cat" "+"))
If someone sees the cat then they chase the dog.
((("someone" "sees" "cat" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the cat and they do not eat the dog then the cat chases the dog.
((("someone" "chases" "cat" "+") ("someone" "eats" "dog" "~")) -> ("cat" "chases" "dog" "+"))
If someone sees the cat and they are round then they eat the bear.
((("someone" "sees" "cat" "+") ("someone" "is" "round" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the cat and they do not chase the dog then the cat is big.
((("someone" "eats" "cat" "+") ("someone" "chases" "dog" "~")) -> ("cat" "is" "big" "+"))
The bear eats the dog.
True
1
proof
[(triple1)]
("bear" "eats" "dog" "+")
triple1
The dog does not see the cat.
False
1
inv-proof
[(triple3)]
("dog" "sees" "cat" "-")
triple3
The dog chases the dog.
True
2
proof
[(((triple3) -> rule3))]
("dog" "chases" "dog" "+")
((triple3) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "chases" "dog" "-")
((triple3) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "-")
The cat chases the dog.
Unknown
rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "dog" "+")
The cat does not chase the bear.
Unknown
inv-random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear eats the dog.[(triple1)] The cat is not round.[(triple2)] The dog sees the cat.[(triple3)] @1: The dog chases the dog.[(((triple3) -> rule3))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The cat is not round.
("cat" "is" "round" "-")
triple2
The dog sees the cat.
("dog" "sees" "cat" "+")
triple3
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple3) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1