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