The bear is kind. The bear is young. The mouse eats the bear. If someone sees the mouse and the mouse sees the bear then they chase the mouse. If someone is kind then they see the mouse. If someone chases the mouse then they see the bear. If someone sees the mouse and the mouse eats the bear then the mouse sees the bear. If someone chases the mouse then they eat the mouse. If the bear eats the mouse then the bear is nice.
The bear is kind.
("bear" "is" "kind" "+")
The bear is young.
("bear" "is" "young" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
If someone sees the mouse and the mouse sees the bear then they chase the mouse.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "bear" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is kind then they see the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "mouse" "+"))
If someone chases the mouse then they see the bear.
((("someone" "chases" "mouse" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the mouse and the mouse eats the bear then the mouse sees the bear.
((("someone" "sees" "mouse" "+") ("mouse" "eats" "bear" "+")) -> ("mouse" "sees" "bear" "+"))
If someone chases the mouse then they eat the mouse.
((("someone" "chases" "mouse" "+")) -> ("someone" "eats" "mouse" "+"))
If the bear eats the mouse then the bear is nice.
((("bear" "eats" "mouse" "+")) -> ("bear" "is" "nice" "+"))
The mouse eats the bear.
True
1
proof
[(triple3)]
("mouse" "eats" "bear" "+")
triple3
The bear is not young.
False
1
inv-proof
[(triple2)]
("bear" "is" "young" "-")
triple2
The bear sees the mouse.
True
2
proof
[(((triple1) -> rule2))]
("bear" "sees" "mouse" "+")
((triple1) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear does not see the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "sees" "mouse" "-")
((triple1) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse sees the bear.
True
4
proof
[(((((triple1) -> rule2) triple3) -> rule4))]
("mouse" "sees" "bear" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The mouse does not see the bear.
False
4
inv-proof
[(((((triple1) -> rule2) triple3) -> rule4))]
("mouse" "sees" "bear" "-")
((((triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear chases the mouse.
True
7
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule4)) -> rule1))]
("bear" "chases" "mouse" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The bear does not chase the mouse.
False
7
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule4)) -> rule1))]
("bear" "chases" "mouse" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The mouse does not chase the mouse.
Unknown
inv-rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse eats the mouse.
Unknown
rconc
[@3: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("mouse" "eats" "mouse" "+")
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 mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The bear is kind.[(triple1)] The bear is young.[(triple2)] The mouse eats the bear.[(triple3)] @1: The bear sees the mouse.[(((triple1) -> rule2))] @2: The mouse sees the bear.[(((((triple1) -> rule2) triple3) -> rule4))] @3: The bear chases the mouse.[(((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule4)) -> rule1))] @4: The bear eats the mouse.[(((((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule4)) -> rule1)) -> rule5))] The bear sees the bear.[(((((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule4)) -> rule1)) -> rule3))] @5: The bear is nice.[(((((((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule4)) -> rule1)) -> rule5)) -> rule6))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple1) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The bear eats the mouse.
("bear" "eats" "mouse" "+")
((((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule2 % int4)) triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The bear sees the bear.
("bear" "sees" "bear" "+")
((((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule2 % int4)) triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
((((((((triple1) -> (rule2 % int5)) ((((triple1) -> (rule2 % int5)) triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int5