The bear chases the dog. The bear chases the mouse. The dog is blue. The mouse is cold. The mouse visits the rabbit. The rabbit chases the dog. The rabbit does not visit the mouse. If someone visits the dog and they chase the bear then the dog chases the mouse. If someone visits the rabbit then the rabbit is green. If someone is cold and blue then they chase the mouse. If someone eats the bear and they chase the mouse then the bear does not visit the dog. If someone is blue then they visit the bear. If someone eats the mouse then the mouse does not visit the bear. If someone visits the mouse then they eat the bear. If the rabbit is green and the rabbit chases the dog then the rabbit visits the bear.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
If someone visits the dog and they chase the bear then the dog chases the mouse.
((("someone" "visits" "dog" "+") ("someone" "chases" "bear" "+")) -> ("dog" "chases" "mouse" "+"))
If someone visits the rabbit then the rabbit is green.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone is cold and blue then they chase the mouse.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "chases" "mouse" "+"))
If someone eats the bear and they chase the mouse then the bear does not visit the dog.
((("someone" "eats" "bear" "+") ("someone" "chases" "mouse" "+")) -> ("bear" "visits" "dog" "-"))
If someone is blue then they visit the bear.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "bear" "+"))
If someone eats the mouse then the mouse does not visit the bear.
((("someone" "eats" "mouse" "+")) -> ("mouse" "visits" "bear" "-"))
If someone visits the mouse then they eat the bear.
((("someone" "visits" "mouse" "+")) -> ("someone" "eats" "bear" "+"))
If the rabbit is green and the rabbit chases the dog then the rabbit visits the bear.
((("rabbit" "is" "green" "+") ("rabbit" "chases" "dog" "+")) -> ("rabbit" "visits" "bear" "+"))
The rabbit does not visit the mouse.
True
1
proof
[(triple7)]
("rabbit" "visits" "mouse" "-")
triple7
The dog is not blue.
False
1
inv-proof
[(triple3)]
("dog" "is" "blue" "-")
triple3
The rabbit is green.
True
2
proof
[(((triple5) -> rule2))]
("rabbit" "is" "green" "+")
((triple5) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple5) -> rule2))]
("rabbit" "is" "green" "-")
((triple5) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the bear.
True
4
proof
[(((((triple5) -> rule2) triple6) -> rule8))]
("rabbit" "visits" "bear" "+")
((((triple5) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not visit the bear.
False
4
inv-proof
[(((((triple5) -> rule2) triple6) -> rule8))]
("rabbit" "visits" "bear" "-")
((((triple5) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The mouse does not chase the bear.
Unknown
inv-random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The bear chases the dog.[(triple1)] The bear chases the mouse.[(triple2)] The dog is blue.[(triple3)] The mouse is cold.[(triple4)] The mouse visits the rabbit.[(triple5)] The rabbit chases the dog.[(triple6)] The rabbit does not visit the mouse.[(triple7)] @1: The dog visits the bear.[(((triple3) -> rule5))] The rabbit is green.[(((triple5) -> rule2))] @2: The rabbit visits the bear.[(((((triple5) -> rule2) triple6) -> rule8))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple6
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple7
The dog visits the bear.
("dog" "visits" "bear" "+")
((triple3) -> (rule5 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple5) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((((triple5) -> (rule2 % int2)) triple6) -> (rule8 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2