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