The cat likes the dog. The dog chases the cat. If someone likes the cat and the cat is green then they are big. If someone likes the dog then the dog sees the cat. If the cat chases the dog then the cat is red. Big people are red. If someone likes the dog then the dog chases the cat. If someone likes the dog then the dog chases the cat.
The cat likes the dog.
("cat" "likes" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
If someone likes the cat and the cat is green then they are big.
((("someone" "likes" "cat" "+") ("cat" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone likes the dog then the dog sees the cat.
((("someone" "likes" "dog" "+")) -> ("dog" "sees" "cat" "+"))
If the cat chases the dog then the cat is red.
((("cat" "chases" "dog" "+")) -> ("cat" "is" "red" "+"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone likes the dog then the dog chases the cat.
((("someone" "likes" "dog" "+")) -> ("dog" "chases" "cat" "+"))
If someone likes the dog then the dog chases the cat.
((("someone" "likes" "dog" "+")) -> ("dog" "chases" "cat" "+"))
The dog chases the cat.
True
1
proof
[(triple2 OR ((triple1) -> rule5) OR ((triple1) -> rule6))]
("dog" "chases" "cat" "+")
triple2
((triple1) -> (rule5 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
((triple1) -> (rule6 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog does not chase the cat.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule5) OR ((triple1) -> rule6))]
("dog" "chases" "cat" "-")
triple2
((triple1) -> (rule5 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
((triple1) -> (rule6 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "big" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat likes the dog.[(triple1)] The dog chases the cat.[(triple2 OR ((triple1) -> rule5) OR ((triple1) -> rule6))] @1: The dog sees the cat.[(((triple1) -> rule2))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The dog chases the cat.
("dog" "chases" "cat" "+")
triple2
((triple1) -> (rule5 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
((triple1) -> (rule6 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
((triple1) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1