The bear sees the dog. The dog chases the mouse. The mouse likes the dog. If someone chases the bear and the bear is cold then the bear chases the dog. If someone chases the dog and they like the bear then they see the dog. If someone likes the mouse then the mouse chases the bear. If someone sees the bear and they are big then the bear likes the dog. If someone likes the bear then they chase the dog. If the dog chases the mouse then the dog likes the bear.
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If someone chases the bear and the bear is cold then the bear chases the dog.
((("someone" "chases" "bear" "+") ("bear" "is" "cold" "+")) -> ("bear" "chases" "dog" "+"))
If someone chases the dog and they like the bear then they see the dog.
((("someone" "chases" "dog" "+") ("someone" "likes" "bear" "+")) -> ("someone" "sees" "dog" "+"))
If someone likes the mouse then the mouse chases the bear.
((("someone" "likes" "mouse" "+")) -> ("mouse" "chases" "bear" "+"))
If someone sees the bear and they are big then the bear likes the dog.
((("someone" "sees" "bear" "+") ("someone" "is" "big" "+")) -> ("bear" "likes" "dog" "+"))
If someone likes the bear then they chase the dog.
((("someone" "likes" "bear" "+")) -> ("someone" "chases" "dog" "+"))
If the dog chases the mouse then the dog likes the bear.
((("dog" "chases" "mouse" "+")) -> ("dog" "likes" "bear" "+"))
The bear sees the dog.
True
1
proof
[(triple1)]
("bear" "sees" "dog" "+")
triple1
The dog does not chase the mouse.
False
1
inv-proof
[(triple2)]
("dog" "chases" "mouse" "-")
triple2
The dog likes the bear.
True
2
proof
[(((triple2) -> rule6))]
("dog" "likes" "bear" "+")
((triple2) -> (rule6 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The dog does not like the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("dog" "likes" "bear" "-")
((triple2) -> (rule6 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The dog chases the dog.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("dog" "chases" "dog" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog does not chase the dog.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule5))]
("dog" "chases" "dog" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog sees the dog.
True
6
proof
[(((((((triple2) -> rule6)) -> rule5) ((triple2) -> rule6)) -> rule2))]
("dog" "sees" "dog" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The dog does not see the dog.
False
6
inv-proof
[(((((((triple2) -> rule6)) -> rule5) ((triple2) -> rule6)) -> rule2))]
("dog" "sees" "dog" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The mouse does not see the dog.
Unknown
inv-rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "dog" "-")
The bear chases the dog.
Unknown
rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "dog" "+")
The mouse does not chase the bear.
Unknown
inv-rconc
[@1: The mouse chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "bear" "-")
The mouse chases the dog.
Unknown
rconc
[@1: The mouse chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "dog" "+")
The dog does not see the mouse.
Unknown
inv-random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
@0: The bear sees the dog.[(triple1)] The dog chases the mouse.[(triple2)] The mouse likes the dog.[(triple3)] @1: The dog likes the bear.[(((triple2) -> rule6))] @2: The dog chases the dog.[(((((triple2) -> rule6)) -> rule5))] @3: The dog sees the dog.[(((((((triple2) -> rule6)) -> rule5) ((triple2) -> rule6)) -> rule2))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple3
The dog likes the bear.
("dog" "likes" "bear" "+")
((triple2) -> (rule6 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3