The bear chases the mouse. The cow eats the bear. The mouse sees the cow. If something eats the bear then the bear sees the cow. If something sees the cow then it chases the cow.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something eats the bear then the bear sees the cow.
((("something" "eats" "bear" "+")) -> ("bear" "sees" "cow" "+"))
If something sees the cow then it chases the cow.
((("something" "sees" "cow" "+")) -> ("something" "chases" "cow" "+"))
The bear chases the mouse.
True
1
proof
[(triple1)]
("bear" "chases" "mouse" "+")
triple1
The bear does not chase the mouse.
False
1
inv-proof
[(triple1)]
("bear" "chases" "mouse" "-")
triple1
The bear sees the cow.
True
2
proof
[(((triple2) -> rule1))]
("bear" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The mouse does not chase the cow.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "chases" "cow" "-")
((triple3) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The cow does not chase the mouse.
Unknown
inv-random
[@0: The cow chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "mouse" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The cow eats the bear.[(triple2)] The mouse sees the cow.[(triple3)] @1: The bear sees the cow.[(((triple2) -> rule1))] The mouse chases the cow.[(((triple3) -> rule2))] @2: The bear chases the cow.[(((((triple2) -> rule1)) -> rule2))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The cow eats the bear.
("cow" "eats" "bear" "+")
triple2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple3
The bear sees the cow.
("bear" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((triple3) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2