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