The bear likes the cat. The bear likes the dog. The bear sees the cat. The cat chases the dog. The dog chases the cat. The dog likes the bear. The dog sees the cat. If something chases the dog and it is blue then the dog is cold. If something sees the dog and the dog likes the cat then it is blue. If something sees the dog and the dog sees the bear then it is cold. If the bear chases the cat and the cat chases the dog then the cat sees the dog. If the bear likes the cat and the bear is young then the cat is nice. If something likes the cat and it likes the bear then the cat sees the bear. If something chases the bear then it chases the dog. If the dog chases the cat then the cat chases the bear.
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat chases the dog.
("cat" "chases" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
If something chases the dog and it is blue then the dog is cold.
((("something" "chases" "dog" "+") ("something" "is" "blue" "+")) -> ("dog" "is" "cold" "+"))
If something sees the dog and the dog likes the cat then it is blue.
((("something" "sees" "dog" "+") ("dog" "likes" "cat" "+")) -> ("something" "is" "blue" "+"))
If something sees the dog and the dog sees the bear then it is cold.
((("something" "sees" "dog" "+") ("dog" "sees" "bear" "+")) -> ("something" "is" "cold" "+"))
If the bear chases the cat and the cat chases the dog then the cat sees the dog.
((("bear" "chases" "cat" "+") ("cat" "chases" "dog" "+")) -> ("cat" "sees" "dog" "+"))
If the bear likes the cat and the bear is young then the cat is nice.
((("bear" "likes" "cat" "+") ("bear" "is" "young" "+")) -> ("cat" "is" "nice" "+"))
If something likes the cat and it likes the bear then the cat sees the bear.
((("something" "likes" "cat" "+") ("something" "likes" "bear" "+")) -> ("cat" "sees" "bear" "+"))
If something chases the bear then it chases the dog.
((("something" "chases" "bear" "+")) -> ("something" "chases" "dog" "+"))
If the dog chases the cat then the cat chases the bear.
((("dog" "chases" "cat" "+")) -> ("cat" "chases" "bear" "+"))
The dog sees the cat.
True
1
proof
[(triple7)]
("dog" "sees" "cat" "+")
triple7
The dog does not like the bear.
False
1
inv-proof
[(triple6)]
("dog" "likes" "bear" "-")
triple6
The cat chases the bear.
True
2
proof
[(((triple5) -> rule8))]
("cat" "chases" "bear" "+")
((triple5) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat does not chase the bear.
False
2
inv-proof
[(((triple5) -> rule8))]
("cat" "chases" "bear" "-")
((triple5) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "blue" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "blue" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The bear likes the cat.[(triple1)] The bear likes the dog.[(triple2)] The bear sees the cat.[(triple3)] The cat chases the dog.[(triple4 OR ((((triple5) -> rule8)) -> rule7))] The dog chases the cat.[(triple5)] The dog likes the bear.[(triple6)] The dog sees the cat.[(triple7)] @1: The cat chases the bear.[(((triple5) -> rule8))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The bear likes the dog.
("bear" "likes" "dog" "+")
triple2
The bear sees the cat.
("bear" "sees" "cat" "+")
triple3
The cat chases the dog.
("cat" "chases" "dog" "+")
triple4
((((triple5) -> (rule8 % int2))) -> (rule7 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The dog chases the cat.
("dog" "chases" "cat" "+")
triple5
The dog likes the bear.
("dog" "likes" "bear" "+")
triple6
The dog sees the cat.
("dog" "sees" "cat" "+")
triple7
The cat chases the bear.
("cat" "chases" "bear" "+")
((triple5) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1