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